Commit 28ce29e0 authored by Felix Freiberger's avatar Felix Freiberger
Browse files

Linguistic improvements.

parent aad88330
......@@ -363,7 +363,7 @@ var workerData;
};
var stateIsWeakConnectionExplored = function (ltsData, stateName) { // if true, no more states may be added to weakConnections
var stateIsWeakConnectionExplored = function (ltsData, stateName) { // if true, no more states will be added to weakConnections
var state = ltsData.core.states[stateName];
if (state.weakConnectionExplored) return true;
......@@ -378,7 +378,7 @@ var workerData;
};
var stateIsFullyWeakExplored = function (ltsData, stateName) { // if true, no more transitions or connection will be added to this state
var stateIsFullyWeakExplored = function (ltsData, stateName) { // if true, no more weak transitions or connections will be added to this state
var states = ltsData.core.states;
var state = states[stateName];
......@@ -908,7 +908,7 @@ var workerData;
}), true);
var outgoingNewTransitions = _.map(outgoingOldTransitions, function (transition) {
// this weak transition points to an old state - build a new one, pointing to a new State
// this weak transition points to an old state - build a new one, pointing to a new state
return {
label: transition.label,
target: oldToNewLabel(transition.target)
......@@ -965,7 +965,7 @@ var workerData;
var newInitialState = oldToNewLabel(ltsData.core.initialState);
// add weak self-loop if needed for observational congruence
// add weak self-loop if needed for observation congruence
var blockWithInitialState = stateToBlockMap[ltsData.core.initialState];
if (_.some(states[ltsData.core.initialState].transitions, function (transition) {
return transition.weak && stateToBlockMap[transition.target] === blockWithInitialState;
......
......@@ -2,7 +2,7 @@
<h1>pseuCo.com User Manual</h1>
<a id="overview"></a><h2>Overview</h2>
<p>With this application, you can easily create and share <a ng-href="#{{path}}#ccs">CCS</a> and <a ng-href="#{{path}}#pseuco">pseuCo</a> files and convert them to <a ng-href="#{{path}}#lts">Labelled Transition Systems</a>. You can also minimize and analyze such transition systems.</p>
<p>The following sections will help you using pseuCo.com.</p>
<p>The following sections will help you to use pseuCo.com.</p>
<a id="requirements"></a><h2>Requirements</h2>
<p>PseuCo.com is designed to run in any modern browser. The most important requirements are:</p>
......@@ -11,12 +11,12 @@
<li><p><b>LocalStorage</b> must be available. This is the default in most browsers. If you receive an error message that LocalStorage it is not available, make sure <i>private browsing</i> is disabled, and try enabling <i>cookies</i> &ndash; some browsers silently block LocalStorage if cookies are disabled.</p></li>
<li><p><b>Cookies</b> are required to switch to the beta version.</p></li>
</ul>
<p>PseuCo.com has been tested in recent versions of Chrome, Firefox, and Internet Explorer.</p>
<p>PseuCo.com has been tested in recent versions of Chrome, Firefox and Internet Explorer.</p>
<a id="files"></a><h2>Managing Files</h2>
<p>Everything you create in this application is saved automatically within your browser. If you go back to <a href="http://pseuco.com/">pseuCo.com</a> on the same device, you will see all files you created in the <a href="#/files">Files</a> tab.</p>
<p>If you did not enter a file name, you might still be able to find your file in the &ldquo;Unnamed Files&rdquo; section. However, such files are deleted automatically after a few days. To keep a file permanently, you must give it a name. To do so, open it, and enter a name into the box at the top of the page.</p>
<p>Your files can be deleted by your browser in some cases, e.g. if you &ldquo;clear private data&rdquo; or use a special &ldquo;private mode&rdquo;. To keep your files safe, you should <a href="#{{path}}#backup">save a backup</a> regularly.</p>
<p>If you did not enter a file name, you might still be able to find your file in the &ldquo;Unnamed Files&rdquo; section. However, such files are deleted automatically after a few days. To keep a file permanently, you must give it a name. To do so, open it and enter a name into the box at the top of the page.</p>
<p>Your files can be deleted by your browser in some cases, e.g. if you &ldquo;clear private data&rdquo; or use &ldquo;private mode&rdquo;. To keep your files safe, you should <a href="#{{path}}#backup">save a backup</a> regularly.</p>
<p>If you want to create a copy of a file, click the <span class="glyphicon glyphicon-plus-sign"></span> clone icon next to its name on the <a href="#/files">Files</a> tab. An unnamed copy of the file will open. To save it permanently, give it a name as usual.</p>
<p>To delete a named file, click the yellow <span class="glyphicon glyphicon-trash"></span> delete button next to it. If the file was named, the name will be removed, causing the file to be deleted after a few days. If you accidentally deleted a named file, open it from the &ldquo;Unnamed Files&rdquo; section, and re-enter a file name.</p>
<p>To delete an unnamed file immediately, click the red <span class="glyphicon glyphicon-trash"></span> delete button next to it. The file will be deleted immediately. <b>Watch out:</b> There is no way to undo this.</p>
......@@ -27,17 +27,17 @@
<p>To restore a backup, open the <a href="#/backup">Backup</a> tab. Copy the backup data from the text file you stored earlier, and paste it into the text box in the &ldquo;Restore&rdquo; section. If your backup is valid, a button will appear below the text box. Read the instructions, and click the button to start the restore process.</p>
<a id="editing"></a><h2>Editing Files</h2>
<p>If you open a file for editing, you will see one or multiple windows, containing an editor. It will look like this:</p>
<p>If you open a file for editing, you will see one or multiple windows, each containing an editor. It will look like this:</p>
<editor:manager editors="demoEditors" settings="settings" fullscreen-mode="false"></editor:manager>
<p>What you see above isn't a static image &ndash; it's a live demo. Feel free to experiment with the windows. Changes you make are ignored and will be lost when you leave this page.</p>
<p>You can resize these windows horizontally by dragging the grey separator bar. In addition, every window has a <span class="glyphicon glyphicon-resize-full"></span> button in the top right corner, which will maximize the window.</p>
<p>If a window shrinks too much, it will be reduced to a thin vertical stripe. To show the contents again, drag a divider to make room for it, or click on the stripe to quickly maximize it.</p>
<p>Only the leftmost window is editable &ndash; it contains your file. All other windows show data generated the file, for example the LTS graph. If you want to edit such generated data, check if the title has an <span class="glyphicon glyphicon-edit"></span> edit icon: If it has, you can click it to create a new file based on the content below.</p>
<p>Only the leftmost window is editable &ndash; it contains your file. All other windows show data generated from that file, for example the LTS graph. If you want to edit such generated data, check if the title has an <span class="glyphicon glyphicon-edit"></span> edit icon: If it has, you can click it to create a new file based on the content below.</p>
<p>To get more information about a specific editor, click the <span class="glyphicon glyphicon-question-sign"></span> help icon on the corresponding title bar.</p>
<p>While editing a file you will see some buttons, called &ldquo;action buttons&rdquo;, on the bottom of the page. You can find more information on them below, or in the section for the corresponding file type.</p>
<h3>File Sharing</h3>
<p>You can easily share any open file by clicking the &ldquo;<span class="glyphicon glyphicon-share"></span> Share this file&rdquo; action button. After accepting the conditions and clicking the upload button, you will be given a special link. You can pass this link on to anyone you want to share this file with.</p>
<p>You can easily share any open file by clicking the &ldquo;<span class="glyphicon glyphicon-share"></span> Share this file&rdquo; action button. After accepting the conditions and clicking the upload button, you will be given a unique link. You can pass this link on to anyone you want to share this file with.</p>
<p>Any user opening a sharing link will see a read-only view of the shared file. The file can be saved and made editable by clicking the blue notification bar.</p>
<a id="import"></a><h2>Importing Files</h2>
......@@ -80,7 +80,7 @@
</ul>
<h4>LTS Minimization</h4>
<p>For any transition system, pseuCom.com can compute the minimal observationally congruent transition system for you. Start this process by clicking the <span class="glyphicon glyphicon-resize-small"></span> Minimize button in the tool bar.</p>
<p>For any transition system, pseuCom.com can compute the minimal observation congruent transition system for you. Start this process by clicking the <span class="glyphicon glyphicon-resize-small"></span> Minimize button in the tool bar.</p>
<p>Fully minimizing the system only works if the transition system has been fully explored. You will see a notice in the upper left corner of the LTS viewer if exploration is not finished yet. You can start the minimization process at any time, but the resulting system may be too large.</p>
<p>If you view a minimized transition system, click the <span class="glyphicon glyphicon-resize-full"></span> Restore button at any time to return to the original transition system.</p>
......@@ -96,7 +96,7 @@
<p>Some export formats fail to describe certain transition systems. Please read the details before proceeding.</p>
<a id="pseuco"></a><h3>pseuCo</h3>
<p>You can find information about the history of pseuCo in the <a href="#/landing">landing page</a>.</p>
<p>You can find information about the history of pseuCo on the <a href="#/landing">landing page</a>.</p>
<p>The following sections give you an overview over pseuCo's syntax and semantics.</p>
<h4>Getting Started</h4>
......@@ -145,7 +145,7 @@
<h5>Channels</h5>
<p>Channels can be synchronous or asynchronous, and have any of the primitive types <code>bool</code>, <code>int</code> or <code>string</code>. Asynchronous channels are declared with a fixed capacity.</p>
<pre:for:copying data="'boolchan chan1; // synchronous, type bool\nintchan7 chan1; // asynchronous, type int'"></pre:for:copying>
<p>Unless full, channels can accept values from a sender. Unless empty, channels can emit values to a receiver, using a use first-in first-out policy:</p>
<p>Unless full, channels can accept values from a sender. Unless empty, channels can emit values to a receiver, using a first-in first-out policy:</p>
<pre:for:copying data="'intchan7 chan2;\nchan2 &lt;! 7; // send 7\nchan2 &lt;! 8; // and send 8\n&lt;? chan2; // receive 7\nint x = &lt;? chan2; // now x will have value 8'"></pre:for:copying>
<p>Attempting to receive from an empty channel blocks the receiver, attempting to send to a full channel blocks the sender. Receiving is destructive.</p>
<p>Arrays come in handy for declaring multiple channels:</p>
......@@ -161,17 +161,17 @@
<h4>Shared Memory</h4>
<p>In pseuCo, several agents may share access to some variables. If of primitive type, such variables need to be declared globally, while instances of structures can also be shared by passing them as arguments (owed to Call-by-Reference).</p>
<p>If an agent can write to some variable, while at least one other agent can read or write the same variable, we are facing a <b>data race</b>. Programs with data races are considered <b>incorrect</b>.</p>
<p>If an agent can write to some variable while at least one other agent can read or write the same variable, we are facing a <b>data race</b>. Programs with data races are considered <b>incorrect</b>.</p>
<h5>Explicit Locking</h5>
<p>The keyword <code>mutex</code> is used to declare a <b>lock</b> (or <b>mutex</b>). Locks are used to coordinate access to data by preventing concurrent access, preventing data races. Locks can be locked with <code>lock</code> and can be unlocked with <code>unlock</code>:</p>
<p>The keyword <code>mutex</code> is used to declare a <b>lock</b> (or <b>mutex</b>). Locks are used to coordinate access to data by preventing concurrent access, preventing data races. Locks can be locked with <code>lock</code> and unlocked with <code>unlock</code>:</p>
<pre:for:copying data="'mutuex m; // declaration\nint i = 5;\n\nvoid dec() {\n lock m; // give it to me\n i--; // no data race\n unlock m; // done\n}'"></pre:for:copying>
<p>There is no built-in correspondence between a lock and the data guarded by that lock. It is the programmers responsibility to make sure every access to the guarded data is protected correctly.</p>
<h5>Implicit Locking</h5>
<p>The keyword <code>monitor</code> instead of <code>struct</code> declares a <b>monitor</b> &ndash; a structure, that makes use of an <b>implicit</b> lock: There is a built-in mechanism that locks this lock <b>before</b> any monitor method call is effectuated and unlocks it only <b>after</b> the method's <code>return</code> has happened. This ensures that the encapsulated data is properly guarded against data races:</p>
<p>The keyword <code>monitor</code> instead of <code>struct</code> declares a <b>monitor</b> &ndash; a structure that makes use of an <b>implicit</b> lock: There is a built-in mechanism that locks this lock <b>before</b> any monitor method call is effectuated and unlocks it only <b>after</b> the method's <code>return</code> has happened. This ensures that the encapsulated data is properly guarded against data races:</p>
<pre:for:copying data="'monitor Count {\n int a = 0;\n int plusPlus() {\n a++;\n return a;\n }\n}'"></pre:for:copying>
<p>Monitor methods may need to wait for specific <b>conditions</b> concerning the data encapsulated by the monitor before effectuating certain operations on them. Conditions are declared with the keyword <code>condition</code>. The waiting is done by <code>waitForCondition</code> which only proceeds once the condition is satisfied. Internally the implicit lock of the monitor is unlocked so as to allow others to proceed and operate on the encapsulated data, so that eventually the condition can become satisfied. Agents can indicate that a condition is now satisfied using <code>signal</code> or <code>signalAll</code>. This wakes up one or all of the agents waiting on the condition, respectively. On re-acquiring the lock, these agents only proceed if that condition is indeed satisfied, if not they will wait again.</p>
<p>Monitor methods may need to wait for specific <b>conditions</b> concerning the data encapsulated by the monitor before effectuating certain operations on them. Conditions are declared with the keyword <code>condition</code>. The waiting is done by <code>waitForCondition</code> which only proceeds once the condition is satisfied. Internally the implicit lock of the monitor is unlocked so as to allow others to proceed and operate on the encapsulated data, so that eventually the condition can become satisfied. Agents can indicate that a condition is now satisfied using <code>signal</code> or <code>signalAll</code>. This wakes up one or all of the agents waiting on the condition, respectively. On re-acquiring the lock, these agents only proceed if that condition is indeed satisfied, otherwise, they will wait again.</p>
<pre:for:copying data="'monitor Count {\n int i;\n condition notNull with (i &gt> 0);\n \n void inc() {\n i++;\n \n // now someone can do a dec()\n signal notNull;\n }\n \n void dec() {\n waitForCondition notNull;\n i--;\n }\n}\n'"></pre:for:copying>
<a id="ccs"></a><h3>CCS</h3>
......@@ -243,7 +243,7 @@
<p>To get examples for valid CCS terms, <a href="#/new/ccs">create a new CCS file</a> and select a template.</p>
<a id="offline"></a><h2>Offline Mode</h2>
<p>The application is available offline automatically if supported by your browser. Just reopen <a href="http://pseuco.com">pseuCo.com</a> to access it.</p>
<p>The application is available offline automatically if supported by your browser. Just reopen <a href="http://pseuco.com/">pseuCo.com</a> to access it.</p>
<a id="faq"></a><h2>Frequently Asked Questions</h2>
<div class="faq-entry">
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment