Home

Interactive Visualization and Minimization of

1. css B app css styles from the main application B 1ib css styles from external libraries v ly fonts contains fonts containing Glyphicon symbols ay ing B icon png the pseuCo com icon PNG version B icon svg the pseuCo com icon SVG version js B app js JavaScript code from the main application B lib js JavaScript code from external libraries B lib min js JavaScript code from external libraries minified B lib min js map source map for lib js for debugging B orker s JavaScript code for the background worker see ay partials B about html UI fragment About tab B ace html UI fragment for including Ace BB actions html UI fragment action buttons B backup html UI fragment Backup tab E debug html UI fragment the hidden Debug tab see section 5 1 B edit html UI fragment file viewing and editing B error html UI fragment displays critical errors B export html UI fragment LTS file export R fetch hinl UI fragment message shown while a shared file downloads files html UI fragment Files tab Bi help html UI fragment Help tab 49 mmm m import html Ul fragment file import E landing html UI fragment main pseuCo com tab R its ntml UI fragment the LTS viewer B newfile html UI fragment new file creation pseucojava html UI fragment the
2. gt t backing the weak transition By definition each such transition can be decomposed into a sequence of transitions s s gt s 5 t We know that weakProcessState must be called on s s and s since they are all reachable s is reachable by assumption s and s because they are reachable from s Case distinction on whether s gt s and s 5 t have both been discovered before weakProcessState searches for weak transitions based on s s 1 Assume s s and s t have both been discovered Then this call to weakProcessState will add s gt t This serves as the base case for the induction with s s and s t 2 Assume not both s s and s t have been discovered yet This is only possible if s Z s or s Z t otherwise both s sf and s 4 t would have been added before during creation of the LTS for initial states when s was discovered by weak exploration which must have occurred beforehand due to the breadth first order or at the beginning of the iteration in weakProcessState When weakProcessState is called on s the weak transition s s is added because s gt s has been added before because s is initial or was discovered during the breadth first traversal and s 5 s is added by this run of weakProcessState Further case distinction on the order in which s gt s and s t are discovered a Assume s sf is discovered after s 5 t When s sf is a
3. The process of generating the transitions and remaining states is called exploration controlled by the ltsExplorer service in the cp tools package It is defined in To start the exploration it sends an exploreLts request to the worker causing it to perform a breadth first search through the transition system computing each state s transitions as they are needed The transitions computed by this search are sent back to 1tsExplorer in the main thread where they are added to the local copy of the transition system ready to be used by the user interface This exploration continues until all states are explored or a fixed number of states have been explored In the latter case exploration resumes if the user reaches a state with unexplored transitions or explicitly requests exploration to resume in the UI 5 10 LTS Visualization and Graph Layout Since LTS are visualized as a graphs rendering them involves graph layout There are many well known graph layout algorithms but most of them cannot be used for pseuCo com because of the restrictions and considerations that apply for this use case e The algorithm should not be overly CPU intensive since it is running in JavaScript possibly on low end devices e The algorithm must allow to add additional states and transitions afterwards and refine the graph layout This is because pseuCo com allows users to view large or even infinite graphs by expanding states one by one When ad
4. grunt registerTask deploy bower install get ace build grunt registerTask serverside deploy appcache grunt registerTask default test deploy Listing B 2 weakProcessState from worker js var weakProcessState function ltsData stateName 39 285 if stateName stateName ltsData extended explorationState weakFrontier shift 4 O draw next state 286 287 var states ltsData core states 288 var state states stateName 289 290 var insertConnection function set value 291 if contains set value 1 292 set push value 293 return true 294 b 295 F 296 297 var insertTransition function set transition 298 if some set function t 1 299 return t source transition source amp amp t target transition target L amp amp t label transition label 300 3 301 set push transition 302 return true 303 304 305 306 var createTransition function preStateName postStateName label 1 307 var veakTransition 308 source preStateName 309 target postStateName 310 label label 311 F3 312 313 insertTransition states preStateName weakTransitions outgoing L weakTransition 314 insertTransition states postStateName weakTransitions incoming b weakTransition 315 316 317 each state transitions function transition index 318 insert self connection to target state 319 var targetS
5. temporary_files old_build tmp temporary_files managed managed components l ace managed_components ace r watch 1 js 4 files src js js tasks test clean tmpbuild worker rename build Fs 37 src css css managed components bower concat app 2 managed components bover bootstrap giyphicons halflings regular x concat 189 190 191 192 193 194 195 196 197 198 199 205 211 215 232 233 234 235 236 237 238 239 html 1 files src xx x html tasks clean tmpbuild rename unbuild copy partials copy index L rename build css 4 files src css tasks clean tmpbuild rename unbuild cssmin rename build b parsers files src js parsers pegjs tasks clean tmpbuild rename unbuild peg AUT concat vorker L rename build Fs peg ccs src node modules PseuCoCo CCSParser pegis dest temporary files CCSParser js options exportVar CCSParser PseuCo src node modules PseuCoCo PseuCoParser pegis dest temporary files PseuCoParser js options exportVar PseuCoParser Fs AUT src src js parsers AUT pegjs dest temporary files AUTParser js options exportVar AUTParser Fa coffee ccs options bar
6. 1 unbuild files sre build dest temporary files build 1 30 grunt loadNpmTasks grunt bover task grunt loadNpmTasks grunt contrib uglify grunt loadNpmTasks grunt contrib cssmin grunt loadNpmTasks grunt contrib jshint grunt loadNpmTasks grunt contrib copy grunt loadNpmTasks grunt contrib clean grunt loadNpmTasks grunt contrib concat grunt loadNpmTasks grunt contrib watch grunt loadNpmTasks grunt contrib coffee grunt loadNpmTasks grunt peg grunt loadNpmTasks grunt browserify grunt loadNpmTasks grunt zip grunt loadNpmTasks grunt curl grunt loadNpmTasks grunt contrib rename grunt registerTask get ace Getjandjunzip the Ace textyjeditor function if grunt file exists managed components ace ace aceVersion zip grunt task run clean ace curl ace unzip ace grunt registerTask test jshint grunt registerTask build peg coffee concat app concat lib concat CCS L concat PseuCo browserify concat vorker uglify lib cssmin copy partials copy fonts copy images copy htaccess copy serverhtaccess L copy index copy version clean oldbuild rename build 1 grunt registerTask appcache copy appcache
7. Instead let tasks normally return a value that indicates failure If a task crashes crashCallback error and the cancellationCallback of the correspond ing task will be called sourcePath is an optional string indicating the path to the JavaScript file containing the worker If it is omitted js worker js is used The return value of this function is an object containing the following properties and methods id is an integer identifying the worker instance that was started terminateWorker finishCallback is a function that requests the worker to be terminated This function must not be called if the worker is already terminating or has terminated finishCallback will be called once the worker has terminated 14 Remark This does not terminate the worker immediately but waits for the current execution to return Cancellation notifications are sent for all pending tasks that could not be executed any more This method will not forcefully terminate a worker that got stuck and there is no method that will Always ensure that all task functions in your worker terminate regularly submitTask taskName data resultCallback cancellationCallback priority sub mits a task to the worker to be executed This function must not be called if the worker is terminating or has terminated taskName is the name of the task to execute as specified when the worker was defined data is a serializabl
8. gt src js post pseucoco js gt managed_components bower underscore underscore js gt temporary_files AUTParser js gt src js worker js gt src js tasks backgroundWorker js 1 dest temporary files build js worker js nonull true J Fs jshint 36 135 145 188 options n n y new Date toString rename unbuild jshintrc true all src js js 1 cssmin combine files temporary files build css app css temporary files build css lib css b css 1 copy partials expand true flatten true src src partials dest temporary files build partials b index src arc index html dest temporary files build index html htaccess arc arc htaccess dest temporary files build htaccess L serverhtaccess src server server htaccess dest temporary files build api htaccess L appcache src src offline appcache dest build offline appcache options process function content 1 return content Y P Fs fonts expand true flatten true src dest temporary files build fonts L images 1 expand true flatten true src src img dest temporary files build img L version src version tat dest temporary files build version txt r clean tmpbuild temporary_files build build build oldbuild
9. nextStateLabeltt 43 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 weakConnectionPostBlocks uniq flatten map block L function stateName 1 return map states stateName weakConnections post L function postStateName 1 return stateToBlockMaplpostStateNamel H true blocks that can be reached by only tau steps x H var oldToNewLabel function oldStateName return blockToStateInfo stateToBlockMap oldStateName label each blocks function block var thisBlockLabel blockToStatelnfolblockl label var outgoing ldTransitions flatten map block function L stateName return states stateName weakTransitions outgoing 1 true var outgoingNewTransitions map outgoing ldTransitions L function transition 1 this weak transition points to an old state build a new L one pointing to a new state return label transition label target oldToNewLabel transition target y 30 remove duplicates var unique utgoingNewTransitions flatten map groupBy L outgoingNevTransitions label function L transitionsWithCommonLabel 4 return _ uniq transitionsWithCommonLabel target 1 true var weaklyReachib
10. 8 Editors Translations and Actions The main features of pseuCo com are pseuCo and CCS file editing viewing LTS the translations pseuCo CCS and CCS LTS and actions like tracing export or file sharing In the code these features are referenced by three terms 1 An editor is the component responsible for viewing and editing data of a specific file type 2 A translation provides a way to convert data from one file type to another 3 An action describes anything a user can actively initiate Actions can be specific to a file type or apply to any file The interaction between editors translations and actions is configured by the value editorConfiguration defined in Ezesss src js ui editorConfiguration js and shown in Listing 5 8 More specifically for each file type it defines 16 e the name of the editor directive that should be used for data of this file type e the translations that should be used when editing a file of this type and e the actions that apply to data of this file type Additionally it defines actions that apply to files of all types Remark There is one crucial difference between the translations and actions property The translations property applies to files of a specific type For example when editing a pseuCo file only the translations defined for the pseuco file type apply Although there is a translation to CCS no further translations from CSS occur unless they are define
11. CCS LTS translation can use this parse tree instead of the CCS string 5 8 1 Translations in the Background The actual translations are performed by the background worker so that the user interface stays responsive This process is initiated by fileEditCtrl which submits a translate task to the background worker This causes the worker to compute all requested translations one by one returning each translation as an intermediate result as it becomes available The parse trees part of the extended data never leave the background worked However they are stored and used internally in the extended data in the worker 5 9 LTS Exploration The result of translations returning a LTS often is extremely large or even infinite rendering the naive approach of computing the full transition system before returning it useless Therefore translations to LTS are handled in a special way The worker only computes the label of the initial state and stores a function generateTransitions that can generate the transitions of this state T This is crucial The parse trees are returned by the external library and are not serializable 17 Figure 5 3 Graphic from http bl ocks org mbostock 3750558 D3 is s built in force layout The resulting system is stored permanently in the worker A version of it without generateTransitions is returned to the main thread including a datald that allows to reference the data stored in the worker
12. PseuCo com has been tested in recent versions of Chrome Firefox and Internet Explorer Managing Files Everything you create in this application is saved automatically within your browser If you go back to pseuCo com http pseuco com on the same device you will see all files you created in the Files tab If you did not enter a file name you might still be able to find your file in the Unnamed Files 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 Your files can be deleted by your browser in some cases e g if you clear private data or use private mode To keep your files safe you should save a backup regularly If you want to create a copy of a file click the clone icon next to its name on the Files tab An unnamed copy of the file will open To save it permanently give it a name as usual To delete a named file click the yellow 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 Unnamed Files section and re enter a file name To delete an unnamed file immediately click the red li delete button next to it The file will be deleted immediately Watch out There is no way to undo this 52 Backing Up and Restoring Your Files To
13. Using branching time temporal logic to synthesize synchronization skeletons Sci Comput Program 2 3 241 266 1982 Paris C Kanellakis and Scott A Smolka CCS expressions finite state processes and three problems of equivalence In Robert L Probert Nancy A Lynch and Nicola Santoro editors Proceedings of the Second Annual ACM SIGACT SIGOPS Symposium on Principles of Distributed Computing Montreal Quebec Canada August 177 19 1983 pages 228 240 ACM 1983 Robert Paige and Robert Endre Tarjan Three partition refinement algorithms SIAM J Comput 16 6 973 989 1987 Amir Pnueli temporal logic of programs In 18th Annual Symposium on Foundations of Computer Science Providence Rhode Island USA 31 October 1 November 1977 pages 46 57 IEEE Computer Society 1977 65 Legal Notes Fidesstattliche Erkl rung Ich erkl re hiermit an Eides Statt dass ich die vorliegende Arbeit selbst ndig verfasst und keine anderen als die angegebenen Quellen und Hilfsmittel verwendet habe Statement in Lieu of an Oath I hereby confirm that I have written this thesis on my own and that I have not used any other media or materials than the ones referred to in this thesis Finverstandniserklarung Ich bin damit einverstanden dass meine bestandene Arbeit in beiden Versionen in die Bibliothek der Informatik aufgenommen und damit ver ffentlicht wird Declaration of Consent I agree to make both versions of my thesis
14. all transition labels including tau compute using weakConnections for tau and weakTransitions otherwise var splitter set of all states having a transition with this label to a L state in partition2 if getSplit partitioni splitter returns a split replace partition1 by the partitions getSplit returned continue with the next pair end if end for end for end repeat var newStates for each partition in partitions add a new state for it to newStates for each outgoing weak transition or tau connection from a state in partition if it is a tau connection to itself continue tau self loops are L superfluous build a corresponding transition to the new state if transition can be reproduced by following a longer chain of weak L connections and transitions ignore the new transition would be superfluous else add the transition to newState end if end for end for var newlInitialState the state corresponding to the partition with initialState if there is a strong tau transition from initialState to another state that ended L up in the same partition add a tau self loop to nevlnitialState end if return newStates newInitialState end procedure 28 Figure 5 9 While having the minimal number of states this system is not minimal in the number of transitions e Instead of only removing a transition in the cases given in Equation 5 1 this algorithm additionally allows a transition s gt s to be
15. classical pseuCo Java compiler B share html UI fragment file upload for sharing svg hinl UI fragment result of SVG export B trace html UI fragment random trace through LTS htaccess configuration file for Apache see index html main HTML file offline appcache configuration file for the Application Cache see version txt describes the version of pseuCo com either testing if built from source locally or a branch name and commit identifier if built on the official server 50 Appendix E User Manual digital printout Remark documentation of the pseuCo language contains work by Kathrin Stark and Holger Hermanns 51 pseuCo com User Manual Overview With this application you can easily create and share CCS and pseuCo files and convert them to Labelled Transition Systems You can also minimize and analyze such transition systems The following sections will help you to use pseuCo com Requirements PseuCo com is designed to run in any modern browser The most important requirements are JavaScript must be enabled LocalStorage must be available This is the default in most browsers If you receive an error message that LocalStorage it is not available make sure private browsing is disabled and try enabling cookies some browsers silently block LocalStorage if cookies are disabled Cookies are required to switch to the beta version
16. computation 3 PseuCo com supports on demand exploration of large or infinite transition systems This integrates well with model checking which often does not require access to the full transition system for example for evaluating existentially quantified properties 6 2 Additional Input Formats Another potential kind of extension is the addition of another input language similar to the current support for pseuCo The infrastructure of pseuCo com is well suited for this type of extension 1 File management and editing is parametrized allowing to easily add new file types Just declaring the new file type in Ese src js files files js and configuring the translations and actions in Eessitery src js ui editorConfiguration js is enough to add the user interface elements to create manage and edit files of this new file type The additional translations can be implemented in the background worker see section 5 7 2 While LTS exploration currently evaluates CCS terms since the only way to create LTS files apart from importing them is the translation CCS LTS this process is encapsulated in the generateTransitions function A translation from any other input to LTS can easily create transition systems that work with the current code by returning transition systems with a new generateTransitions function 6 3 New Translations for Existing File Types PseuCo com can be extended by new translations for existing f
17. differences compared to simple graphs 1 In LTS states may have self loops 2 In LTS edges are directed and states can be connected by edges in both directions simultaneously 3 In LTS edges are labelled and states can be connected by arbitrarily many edges differing in their label To account for these changes pseuCo com introduces one additional invisible control node per transition This node behaves just like the visible nodes representing states and serves as the control point for a B zier curve representing the transition This change has three main effects 1 Self loops automatically repel each other so they point in different directions and don t overlap as shown in Figure 5 4a 2 Multiple transitions between two states bend slightly so all of them are visible as shown in Figure 5 4b 3 Since the control nodes repel each other they indicate places where short labels can be placed without overlapping as shown in Figure 5 4c This approach often produces decent results like the one shown in In some cases nodes get stuck in a suboptimal position between other nodes as shown in In these cases users can drag and drop nodes to move them manually This works well in practice Because of the virtual springs just dragging one misplaced node moves its neighbours as well often fully untangling the graph with only a single manual intervention 5 11 LTS Minimization PseuCo com can minimize labelled transi
18. grunt contrib cssmin 0 10 0 gr nt contrib copy 0 56 0 grunt contrib clean 0 6 0 grunt contrib concat 0 5 0 gr nt contrib vateh 0 6 1 Nerunt peg ck grunt contrib coffee 0 11 1 pru nt bDrowserify 2 1 4 Gruntezip 0 16 0 1 e2 0 2 grunt contrib rename 0 0 3 1 dependencies PseuCoCo git github com Biewer PseuCoCo git v0 6 26 3 If the specified version of Ace is missing download and unzip it 4 Call PEG js to create the parsers for all grammars 5 Compile the CoffeeScript files from 6 Bundle up all JavaScript files from to pseucoco js using 7 Concatenate all JavaScript files from the external libraries to a single file lib js and minimize it by removing unnecessary white space resulting in lib min js 8 Concatenate all main JavaScript files to app js 9 Concatenate and minify all files from libraries to lib css 10 Concatenate and minify all files from the main application to app css 11 Concatenate the JavaScript files needed for the background worker to worker js see for details 12 Copy all the generated and static files to Espssesi build to build the final directory structure the web server should present 5 4 Application Start Up PseuCo com heavily relies on AngularJS All core functionality is implemented as AngularJS and Remark AngularJS heavily influences the design of JavaScript applicati
19. https connect microsoft com IE feedback details 781964 Then tick this box do not show arrowheads After you ve done that the arrows will be rendered without the arrowhead unluckily this means you cannot see the direction of the arrow but at least they will be rendered at all If Microsoft fixes this bug in a future version of Internet Explorer uncheck the box above to render the arrowheads again If you do not want to wait try to use another https www google com intl de chrome browser browser http firefox com On my mobile device the text editor has some issues for example the backspace key is not working reliably We are sorry the text editor we are using has issues with soft keyboards in some browsers You can try switching to a different browser Please report this issue and provide additional details about your device browser and how to replicate this issue so we can try to fix it In the meantime you can try ticking this box do not use the advanced text editor If you do so you will not see the normal text editor but a simple text box This should work without issues but you will see no error messages in the editor On one of my devices the application just shows a blank screen This can occur if a corrupted version of the application is downloaded Please contact us with details so we can try to fix this issue In the meantime try to clear the application cache which is different f
20. integrated into the user interface PseuCo com features an internal file system for supported file types with extensive import and export capabilities A link based file sharing mechanism enables users to easily send pseuCo com files to any user without requiring anything but an internet connection and a modern browser from the receiver Preliminaries 2 1 pseuCo PseuCo is a programming language designed to teach concurrent programming It features a heavily simplified Java like syntax and has built in support for message passing inspired by Go PseuCo was created by Christian Eisentraut and Holger Hermanns at the chair for Dependable Systems and Software at Saarland University to be used in the mandatory Bachelor level lecture Nebenlaufige Programmierung Concurrent Programming 3 2 2 CCS The Calculus of Communicating Systems CCS is a process calculus designed to model communicating systems There are multiple versions of CCS In this context a pragmatic extension of CCS supporting value passing of booleans integers and strings sequencing and termination is used 1 The semantics of a CCS process is a Labelled Transition System LTS 2 3 Previous Work For his Bachelor s thesis I Sebastian Biewer developed a translational semantics for pseuCo based on CCS His work includes a JavaScript compiler from pseuCo programs to CCS terms a parser for CCS and the CCS operational semantics yielding transition systems as under
21. only significant delay is network access PseuCo com however performs many long running CPU intensive tasks Without countermeasures these would cause the UI to hang for excessive amounts of time The only way to fully prevent this type of issue is by using multi threading JavaScript was designed as a single threaded scripting language and has no memory model Therefore the only widely implemented mechanism of using multiple threads in JavaScript Web VVorkers solely use a message passing interface for communication betvveen the threads The Web Worker API defines methods to start a worker which runs a script file specified when the worker is initialized and to exchange messages with it but provides no further assistance to manage tasks that should be executed by the worker For pseuCo com a new framework was developed to simplify the definition and use of workers that process specific tasks submitted to them by AngularJS applications It is contained in the cp tasks module and consists of the files in the Gree src js tasks directory This framework is intentionally kept general so it can be reused by other projects 5 7 1 Features of the Tasks Framework The tasks framework has the following responsibilities 1 Manage start up and termination of the workers 2 Manage callbacks that hand back computation results and cancellation notifications 3 Ensure that tasks are executed according to their priority which can be
22. with a passing grade accessible to the public by having them added to the library of the Computer Science Department Saarbr cken 30 09 2014 Felix Freiberger
23. 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 G edit icon If it has you can click it to create a new file based on the content below To get more information about a specific editor click the help icon on the corresponding title bar While editing a file you will see some buttons called action buttons on the bottom of the page You can find more information on them below or in the section for the corresponding file type File Sharing You can easily share any open file by clicking the Share this file 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 53 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 Importing Files You can import Labelled Transition Systems into pseuCo com Simply open the import page for transition systems and paste data in a supported file format See the import page for details on which formats are supported In the rare case that the data you pasted can be interpreted in various formats you will see multiple import buttons Make sure you select the correct one so your data will be interpreted correctly Distraction Free Editing To edit files wi
24. 90 return todo 791 1 792 793 var getIncomingActionPredecessors function block gets a map L of all strong actions to predecessor states 794 if block incomingActionPredecessors return block b incomingActionPredecessors 795 796 var result 1 797 798 each block function stateName 799 each states stateName weakTransitions incoming function L transition 800 var label transition label 801 var preList resultllabell 802 if preList preList resultllabell preList 803 preList push transition source 804 H 805 J 806 807 block incomingActionPredecessors result 808 return result 809 Fs 810 811 var getWeakPredecessors function block 812 return _ flatten _ map block function stateName 813 var state states stateName 814 return state weakConnections pre 815 1 true 816 3 817 818 var getSplit function block splitter 819 var intersection _ intersection block splitter 820 if _ isEmpty intersection 1 821 var difference _ difference block splitter 42 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 if isEmpty difference 4 return block1 inters
25. Interactive Visualization and Minimization of Labelled Transition Systems Felix Freiberger Saarland University Natural Sciences and Technology I Computer Science 30 09 2014 Bachelor s Thesis Reviewers Univ Prof Dr Ing Holger Hermanns Univ Prof Dr Verena Wolf Contents 1 Introduction 2 Preliminaries 2 05 LT D 2 XO OS OL 2 3 Previous Work 2 4 Explanation of Symbols and Technical Terms 3 Accessing pseuCo com 3 1 Accessing the Online Version of pseuCo com 4 User Manual 5 Developer Manual 5 3 The Build Process 5 4 Application Start Up 5 5 How pseuCo com Stores and Handles Files 5 6 Offline Model DENIM 5 55 5 10 LTS Visualization and Graph Layout PER RRR Z 2 ds 2 5 12 The Server Component of pseuCo com 5 13 A Build Server for pseuCo com The Future of pseuCo com 6 1 Model Checking 6 2 Additional Input Formats 6 3 New Translations for Existing File Types Bibliography This document is based on version 28ce29e0c1e78581f88a7674e60fd6de41d893f2 of pseuCo com tagged thesis 3 2 Building pseuCo com from Source Ee Re gt w or Ol 32 32 32 32 34 35 47 49 51 63 65 Introduction Labelled transition systems LTS are a popular way of modelling the behaviour of reactive systems and proces
26. ORK TREE CHECKOUT DIR git checkout f quiet 1 is GIT VERSION git rev parse 1 i9 cd CHECKOUT DIR 21 echo Installing NPM packages 22 npm install 24 echo Pruning NPM packages 25 npm prune 26 27 if 1 master 28 then 29 echo Starting server 30 svc u home fefrei service cpw server si fi 32 33 echo Writing version information 34 echo 1 GIT VERSION gt version txt 35 36 echo Deploying 37 grunt serverside 38 39 exit 4 Start the server if it was stopped earlier 5 Run the serverside task of the build script which performs the normal build and generates a configuration file for the HTML Application Cache see 31 The Future of pseuCo com PseuCo com has been designed to be easily extensible featuring many self contained reusable modules This section points out some possible extensions and evaluates how well the existing infrastructure supports them 6 1 Model Checking A useful potential extension is model checking allowing users to verify their transition systems against a LTL 6 or CTL property The infrastructure of pseuCo com is well suited for this extension 1 The user interface is prepared for this addition Model checking could be implemented as an action see section 5 8 similar to tracing and LTS export 2 Model checking is computationally expensive With the tasks API see section 5 7 there already is an extensive infrastructure for background
27. a button to create this type of file on the Files tab allowEmpty boolean if enabled allow to create an empty file of this type allowTemplate boolean if enabled show templates for this file type and allow creating a new file based on them allowImport boolean if enabled allow to import files of this type allowFork boolean if enabled allow the user to create a file of this type based on the result of a translation importableFilesStatement string human readable string explaining which types of text files can be imported for this file type Figure 5 1 Explanation of the properties of a fileType definition Listing 5 6 The configuration file for the application cache offline appcache CACHE MANIFEST version txt js app js js worker js js lib min js css app css css lib css partials about html partials ace html partials actions html partials backup html partials debug html partials edit html partials error html partials export html partials fetch html partials files html partials help html partials import html partials landing html partials lts html partials newfile html partials pseucojava html partials share html partials svg html partials trace html fonts glyphicons halflings regular fonts glyphicons halflings regular fonts glyphicons halflings regular fonts glyphicons halflings regular img icon png eot svg ttf woff NETWORK api 11 An update has been downloaded You can switch to t
28. a result For example in Figure 5 7d the weak connection C D is added since C C and D 5 D This causes two searches 1 A search for all weak transitions ending in C finds A C and B 4 C This causes the weak transitions A D and B D to be added 2 A search for all weak transitions starting in D does not find any transitions Correctness of Weak Transition Computation Correctness of this algorithm assuming it runs to completion can be shown in two steps Lemma 1 The sets in weakConnections are computed correctly as specified in subsection 5 11 1 Proof Soundness can be shown by induction over the program execution The initial state only the initial state has a 7 self loop is sound Whenever a transition s Z t is added to weakConnections it either has the form s gt s which is always a valid weak transition or it is added as the combination of two weak transitions s S s and s t that have been added before both sound by induction For completeness we need to show that every weak r transition s t is added to weakConnections during weak exploration if s and t are both reachable Each such transition is by definition based on a sequence of n N r transitions s gt s gt s2 gt 5 1 gt t with n 1 intermediate states We use induction to show the following version of the claim For any n N any weak transition s t based on a sequence of n intermediate states has been added to weakConn
29. aste add allows to submit files and retrieve a sharing URL for it Requests to this path must be POST requests having a JSON encoded body containing an object with the following properties a file must be an object representing the file to be shared It must have the properties type and content and may have a name b sharingAgreementVersion must be a number representing the version number of the legal notice the user agreed to before uploading the file The server will reject uploads not having a recent enough sharingAgreementVersion C temporary is an optional value If it evaluates to true the server will only store the uploaded P y file for a short amount of time 29 The server will store the submitted file either permanently in the server data paste directory or in memory for temporary shares and return a JSON encoded response It has the following properties a id is the identifier of the file as chosen by the server b url is a URL which can be given to other users to view this file c temporary true will be set for temporary shares Otherwise this property is omitted 2 fAFLLasUmL paste get allows to get files that have been submitted to the server Requests to this path must be GET requests and have one parameter id which is the identifier for the shared file The server will then return a JSON object having the following properties a file will be the file object that was submitted to the ser
30. ate nextDataId var newLtsData core initialState newInitialState states newStates extended 14 datald datald F var generateRelayingTransitionGenerator function state L underlyingStateName 1 return function 1 var underlyingState stateslunderlyingStateNamel if underlyingState transitions blindExploreState data L dataId ltsData underlyingStateName 45 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 var underlyingTansitions underlyingState transitions state transitions state transitionsFromMinimization if state transitions state transitions 11 _ each underlyingTansitions function underlyingTransition L t if stateToBlockMap underlyingTransition target 1 var newStateLabel U nextStateLabel var newState JSON parse enhancedStateTemplate newState generateTransitions L generateRelayingTransitionGenerator nevState L underlyingTransition target newStates newStateLabel newState var newBlock newState stateToBlockMap underlyingTransition target bL newBlock blockToStateInfo newBlock label newStateLabel b else if _ some state transitions fun
31. backup your files open the Backup tab In the Backup section you will see a text box containing all your files Select all text by clicking into it then copy it Paste the contents into an empty text file and store it Please note that unnamed files will not be included in the backup To restore a backup open the Backup tab Copy the backup data from the text file you stored earlier and paste it into the text box in the Restore 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 Editing Files If you open a file for editing you will see one or multiple windows each containing an editor It will look like this pseuCo 1 mainAgent 2 println Hello World 3 S printIn Hello World o 9 O No issues o Minimize Collapse all What you see above isn t a static image 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 You can resize these windows horizontally by dragging the grey separator bar In addition every window has a z button in the top right corner which will maximize the window 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 Only the leftmost window is editable it contains
32. ction transition return transition label underlyingTransition label amp amp transition weak L underlyingTransition weak amp amp transition target L oldToNewLabel underlyingTransition target b 4 return transition already exists ignore Y J state transitions push label underlyingTransition label weak underlyingTransition weak target oldToNewLabel underlyingTransition target H H 3 var safeDataCopy JSON parse JSON stringify newLtsData restore explore functionality for not fully explored states each notFullyWeaklyExploredS8tates function originalStateName 4 var state nevStatesloldToNevLabel originalStateName l state generateTransitions generateRelayingTransitionGenerator L state originalStateName hide transitions from view state needs to be explored state transitionsFromMinimization state transitions state transitions undefined H workerState data dataId newLtsData return data command minimized data safeDataCopy taskCompleted true 1 46 Appendix C The Repository Structure In the source code repository of pseuCo com you can find a multitude of files and directories Some of them are generated by the package managers and the build script and not included in the repository directly Here is an overview over this directory structure aw git hidden data directory from Git f bower compone
33. d in the pseuco property e The actions property applies to data of the file type specified For example the actions defined for lts are available when editing a CCS file since the CCS LTS translation makes LTS data available File editing is handled by the fileEditCtrl and the edit html fileEditCtrl is responsible for setting up the data structures for all editors and actions that are available Given this data the editorManager and actionManager directives are responsible for displaying the editors and action buttons There is one core difference between the data stored in files and the data used by editors translations and actions While files store only the minimal amount of information needed to recreate everything that is visible to the user the in memory representation of data stores additional temporary information that is generated from the persisted data To separate these parts the in memory representation is a JavaScript object with two properties The core property stores the part of data that will be persisted and may have an arbitrary type The extended property stores an object containing all additional in memory only data For example this mechanism makes sure that when viewing a pseuCo file the CCS term shown never has to be parsed While the translation pseuCo CCS yields the CCS string which is the core of the translation in addition it contains the parse tree in the extended part of the data The
34. data ss prestate iterates over all states where s3 gt s is already known stored in the set weakConnections pre of s and s4 poststate iterates over all states where 82 gt s4 is already known stored in the set weakConnections post of s2 For example in Figure 5 7c the transition B gt C is processed This adds the transition A C since B and C C and B 5 C since B B and C C However no weak transitions ending in state D are found since the weak connection C D has not been found yet If the transition is a T transition o 7 the algorithm first adds all new weak connections 3 gt si ss prestate iterates over all states where ss s is already known stored in the set weakConnections pre of s and s4 poststate iterates over all states where s2 S s4 is already known stored in the set weakConnections post Of sz Since adding a weak connection might give rise to new weak transitions by prolonging already computed ones for every weak connection s3 s4 the algorithm adds it searches for every already computed weak transition 55 Es 3 OT S4 86 by iterating ss over weakTransitions incoming of s3 and sg over weakTransitions outgoing of s4 and adds the new transition ss A 84 OF 53 5 S6 respectively Remark The second part of this search extending the beginning of weak transitions is relevant in cyclical graphs only Figure 5 8d shows an example were this search yields
35. dded the resulting iteration will use s S t added by then by induction to add s S t 25 e U P orton 23 24 25 26 27 Listing 5 10 PseudoCode for stateIsFullyWeakExplored procedure stateIsWeakExplored state return whether state has been weak explored end procedure procedure stateIsWeakConnectionExplored state if the state has been marked as weak connection explored return true if stateIsWeakExplored state amp amp every state in weakConnections post fulfulls L stateIsWeakExplored mark this state as weak connection explored return true else return false end if end procedure procedure stateIsFullyWeakExplored state if weak exploration of the LTS is finished already return true if state has been marked as fully weak explored return true if not stateIsWeakConnectionExplored state return false if every target state of a transition in state weakTransitions outgoing fulfills L stateIsWeakConnectionExplored mark state as fully weak explored return true else return false end if end procedure b Assume s 2 t is discovered after s gt s When s t is added the resulting iteration will use s s added by then by induction to add s t All cases have been considered M VVhen VVeak Fxploration Did Not Finish If the breadth first traversal of the graph is interrupted at any point the initial fragment of the graph is likely to already contain all weak transitions al
36. ding new states existing states should not move significantly to ensure the user still can easily recognize them e Since pseuCo com is an interactive application and is even running on touch enabled devices in many cases allowing the user to influence the graph layout is both feasible and desirable To provide the best graph layout possible in this specific application pseuCo com uses force based graph layout The implementation is based on s force layout but adds some tricks to apply the algorithm to transition systems LTS visualization including graph layout is implemented in the ltsEditor directive defined in src is ui directives ltsEditor is s force layout successfully layouts graphs as shown in Figure 5 3 It does so by applying three kinds of forces e A simulated electrical charge of nodes ensures sufficient distance between the nodes Sseelhttps github com mbostock d3 viki Force Layout demonstration http bl ocks org mbostock 929623 18 a Self loops b Multiple transitions c Placement of labels Figure 5 4 Advantages of using control nodes indicated as dark dots usually invisible e Virtual springs along the edges try to keep them at a specified target length e Virtual gravity centres the whole graph Additionally there is a temperature mechanism slowly increasing a virtual friction like effect until all nodes have stopped moving This approach does not suffice for LTS which have some
37. e Ace text editor is an additional dependency Since it is not available as a package it is downloaded and unzipped programatically by a build script 5 3 The Build Process PseuCo com can be built from source using the included build mechanism refer to for an explanation In this section you can find additional information on its internal functionality Running npm install installs all dependencies listed in Listing 5 2 including and corresponding plug ins Afterwards running grunt executes the default task defined in Listing B 1 This task performs the following actions 1 Test the code with ishint to find common programming errors 2 Call Bower to install all dependencies from Listing 5 1 Listing 5 1 Dependency section from bower json dependencies 1 bootstrap 3 2 0 angulat 51 2 29 angular strap 2 0 5 angular animate 1 2 23 engular ro te 1 2 23 angular motion 0 8 3 angular sanitize 1 2 23 angularLocalStorage 0 1 7 underscore ef T 0 momentjs 2 8 2 hammeris 2 0 2 Yan Wed s qq bootstrap additions 0 2 3 jquery 2 1 1 jquery cookie 21 4 1 10 in 12 13 14 15 16 7 18 19 20 21 22 23 24 25 26 27 28 Listing 5 2 Dependency section from package json devDependencies 1 grunt 044 5 grunt bover task 0 4 0 gprunt contrib uglify 50 b 1 grunt contrib Jshint 0 10 0
38. e true files temporary files CCS no parser js node_modules PseuCoCo CCs L coffee node modules PseuCoCo CCSRules coffee node modules L PseuCoCo CCS Traces coffee node modules PseuCoCo CCSExecutor coffee node modules PseuCoCo CCSExport coffee l Fs PseuCo options bare true Fs files gt temporary_files PseuCo_no_parser js node modules PseuCoCo PseuCo L coffee modules PseuCoCo PCType coffee node modules L PseuCoCo PCEnvironment coffee node modules PseuCoCo PCExport L coffee l CCSCompiler options bare true Fa files temporary files CCSCompiler js node_modules PseuCoCo PCCCompiler L coffee node modules PseuCoCo PCCProcessFrame coffee node modules PseuCoCo PCCProgramController coffee node modules PseuCoCo PCCContainer coffee node modules PseuCoCo PCCCompilerStack coffee node modules PseuCoCo PseuCo Compiler coffee node modules PseuCoCo PCCExecutor coffee node modules PseuCoCo PCCExport coffee l 38 252 259 295 305 309 310 311 312 313 284 browserify PseuCoCo src src js pseucoco js dest temporary files pseucoco js Fs options browserifyOptions paths temporary files Fs rename build 4 files src build dest temporary files old build 1 src temporary files build dest build
39. e defined inductively on o Li co Jj c Hnc 8198 28 2689086 8 Definition 3 Weak Transition For any transition system LTS S so the weak transition relation is defined as follows where a Act V r ss dneN ses s s ie Js s S s s 5 Definition 4 Weak Bisimulation For two transition systems LTS S gt s so and LTS 4 10 over the same set Act a relation R C S x T is called weak bisimulation if for any s R and a Act both of the following conditions hold e If s 5 s then there is a t T such that t and s t R e If t then there is a s S such that s s and 5 R Definition 5 Weakly Bisimilar Two transition systems DTS S gt s so and LTS T gt to over the same set Act are called weakly bisimilar LTS LTS if there is a weak bisimulation R such that so to R holds Definition 6 Observation Congruent Two transition systems LTS S gt s so and LTS T to over the same set Act are called observation congruent LTS LTS if both of the following conditions hold If so s then there are n m N and T such that to TA Y and S s T t e If to t then there are n m N and s S such that so T s and S o s T t 34 Appendix B Code Listings Listing B 1 Gruntfile js the co
40. e object that will be sent to the worker and used to call the task function resultCallback is a function that processes results returned by the worker It will be called as resultCallback data taskCompleted where data is the data the task function returned and taskCompleted indicates whether the task has finished or is still computing cancellationCallback is a function that will be called if the task is cancelled for any reason priority is a number in the range 0 9 where 9 indicates highest and 0 lowest priority Tasks with a higher priority are executed before any tasks with a lower priority The function returns a task id that can be passed to cancelTask cancelTask taskId is a function that requests the specified task to be cancelled This function must not be called if the worker is terminating or has terminated The task will be cancelled as soon as possible If the task is currently running it will be stopped the next time it returns After cancelTask has been called all results from this task will be silently dropped This ensures that while a task might finish after you tried to cancel it you can be guaranteed to never receive results from a task that you requested to be cancelled Remark The tasks framework executes all callbacks in an AngularJS context is called automatically and exceptions are sent to exceptionHandler There is no need to call apply manually If you do not understand t
41. ected behaviours cause the browser to keep the application cache and not download any updateq 4Instructions on how to to so are available at help faq blankscreen 5Doing so would be useless since they will be stored in the fully separate HTML Application Cache anyway 12 4 Clearing the normal browser cache will not ensure you see the most recent version as in most browsers the application cache needs to be deleted separately 5 While you can change the API path on the debug page see ection 5 1 the browser will block access to any location not listed in the manifest To ease development the build scripts normally omit the application manifest disabling the offline mode This causes a 404 not found error for the manifest during testing which is expected and causes no further issues To copy the application manifest and enable offline mode execute the appcache build task which is part of the serverside task the official build server runs This is intended behaviour and makes sure that users can keep using their offline applications when they are in a captive network that redirects all HT TP requests to a login page 5 7 Tasks and the Background Worker Normal JavaScript applications are single threaded and use multiple threads only when accessing asyn chronous browser APIs for example for network access This is fine since most JavaScript applications only perform small actions where the
42. ection block2 difference return false var performSplit function block split var index blocks indexOf block if index gt 1 blocks splice index 1 else throw trying to split aynonexisting block blocks push split block1 blocks push split block2 var assignBlock function block return function stateName stateToBlockMaplstateNamel block I 3 each split block1 assignBlock split block1 each split block2 assignBlock split block2 J partition while done done true var todo buildToDo todoloop while isEmpty todo var task todo shift var blocki task blocki if contains blocks block1 continue this block vas b split already var block2 task block2 var veakPredecessors getWeakPredecessors block2 var veakSplit getSplit block1 weakPredecessors if veakSplit done false performSplit block1 veakSplit else var incomingActionPredecessors2 L getIncomingActionPredecessors block2 for var action in incomingActionPredecessors2 var predecessors incomingActionPredecessors2 action b J var split getSplit blocki predecessors if split 1 done false performSplit block1 split break todoloop partitioning completed var nevStates f var nextStateLabel 0 var blockToStatelnfo _ each blocks function block blockToStateInfo block label
43. ections after weakExploreState has been called with s and the intermediate states 1 92 9n 1 Let n N be a fixed natural number and the claim be valid for any m N with m n Case distinction on m 22 9 0 0 60 a The original transition system O O O ays ses b weakProcessState A a 255502 227 SU 9 60 E rm s W c weakProcessState B a w wet BRL Pid a a b s f Result of vveak exploration Dashed arrows represent an element of weakTransitions while dotted arrows represent an element of weakConnections States with double borders are already weakly explored Thick lines indicate the state that is currently being processed and the weak transitions and connections that are added as a result Figure 5 7 How weak exploration processes a transition system 23 v 14 15 16 17 18 19 20 21 22 23 24 26 27 28 29 a The original transition system veakProcessState B d weakProcessState C For an explanation of the different types of lines see Figure 5 7 Figure 5 8 How weak exploration processes a cyclic transition system Listing 5 9 PseudoCode for weakProcessState procedure weakProcessState state for each transition from state add transition target to its own weakConnections pre and weakConnections post L sets if transition is a tau transit
44. et of reachable states After having been run in a breadth first manner for all reachable states veakProcessState O guarantees the following 1 For each state s Steach states s weakConnections pre is an array representing the following set s Sreach s 2 2 For each state s Sreach states s weakConnections post is an array representing the following set s dad s s 3 For each state s Steach States s weakTransitions outgoing is an array representing the following set s 0 8 a s 7 Sreach 4 For each state s Sreach States s weakTransitions incoming is an array representing the following set 650 3 a r s Sreach Listing 5 9 shows a simplified PseudoCode version of weakProcessState while Listing B 2 shows the actual JavaScript implementation The behaviour of this procedure is illustrated in Figure 5 7 The PseudoCode version assumes that the initial state is contained in its own weakConnections pre and weakConnections post sets by default 21 When weakProcessState is called on a state it iterates over all outgoing normal transitions s gt s After adding the transition s s to the corresponding weakConnections sets the algorithm distinguishes between 7 transitions and non 7 transitions e If the transition is not a T transition a Z r the algorithm adds all weak transitions ss s4 it can find using the already computed
45. g specs web apps current work multipage webstorage html o 0 40 wc 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 Listing 5 6 It contains a list of all files belonging to the applicatiom Listing 5 5 fileTypes declaration from files js value fileTypes 4 ccs fullName CCS allowCreation true allowEmpty true allowTemplate true allowImport false allowFork true importableFilesStatement no formats for this file type r pseuco 1 fullName pseuCo allowCreation true allowEmpty true allowTemplate true allowImport false allowFork true importableFilesStatement no formats for this file type lts fullName LTS allowCreation true allowEmpty false allowTemplate false allowImport true allowFork false noWatch true importableFilesStatement pseuCo com LTS JSO0N files and AUT files the key files and one key per file for the actual content In the same module there is a configuration value called fileTypes shown in Listing 5 5 For each allowed file type it defines multiple properties which are explained in Figure 5 1 5 6 Offline Mode Albeit being a web application pseuCo com is available offline This is achieved by using the HTML Application It is configured using the manifest file rzes src offline appcache shown in These files will be downloaded automatically by any browse
46. he Application Cache see section 5 6 4T B index html main HTML file describing the core parts of the UI Additional UI elements partials are injected during runtime B cffline appcache configuration file for the Application Cache see f temporary files location for temporary files needed during the build process B m pi ESEPEEEEPEIE gitattributes configuration file for Git ensuring line endings are normalized gitignore configuration files for Git ensuring generated files are not committed to the repository by accident jshintrc configuration file for bower json configuration file for Bower listing dependencies COPYING license text Gruntfile js configuration file for grunt describing the build process see package json configuration file for pm describing this package and the dependencies ReadMe md version txt contains the string testing to allow pseuCo com to identify itself as having been built from source For the official builds this file is overwritten with the string displayed at amp about 48 Appendix D The Build Directory Structure This section describes the final directory structure ready to be served by Apache or any other HTTP server It is set up by the build scripts in build fl api virtual path to which the server component should respond The folder contains a htaccess file to configure to redirect requests to it
47. he new version now Figure 5 2 Notification bar after the application cache was updated Listing 5 7 A configuration file Apache to configure client side caching AddType text cache manifest appcache Header set Cache Control no cache must revalidate lt Files offline appcache gt Header set Cache Control must revalidate lt Files gt When an update is available and the user opens pseuCo com the request is served from the cache Afterwards the browser requests the manifest file determines that an update is available and downloads the new version To inform the user about this pseuCo com listens to events emitted by the browser to determine the update status shows a progress bar during the download phase and shows a notification bar see Figure 5 2 offering to switch to the new version afterwards This behaviour is implemented in Gaston src js app js It is important to ensure that the application cache never contains invalid versions of the application because otherwise the user s browser will only re download the corrupted files when an update is released or the user manually clears the application cachd The HTML Application Cache has an integrated mechanism to ensure that if the application is updated on the server during the download phase the download process which would save a mixture of old and new files fails safely After the download finishes the browser fetches the application manifest fi
48. he previous paragraph you can ignore it safely 5 7 4 Usage of the Tasks Framework for pseuCo com The tasks framework powers all CPU intensive computations on pseuCo com For all of the following the computation is run by a task in the background worker and only the results are sent to the main thread to be displayed in the UI all translations see section 5 8 LTS exploration see section 5 9 LTS random tracing LTS export LTS minimization see section 5 11 parsing of file imports 15 25 26 27 28 29 31 32 33 34 35 36 37 38 39 40 41 42 43 44 46 47 48 Listing 5 8 The configuration file editorConfiguration js angular module cp ui value editorConfiguration fileTypes 1 ccs editor ace text editor translations 1 source ccs target lts 1 actions r pseuco editor ace text editor translations t Source pseuco target ccs r 1 source ccs target lts Y 1 actions r 1689 4 editor lts editor translations actions i displayIcon glyphicon glyphicon road displayName Random path action traceLts i t displayIcon glyphicon glyphicon export displayName Export LTS action exportLts Y fileActions 1 displayIcon glyphicon glyphicon share displayName Share this file action shareFile b 1 1955 5
49. his condition false negative resulting in a system with too many transitions As explained in the beginning of this is an accepted behaviour When all weak transitions have been computed minimization is guaranteed to be complete Correctness of this approach follows from the correctness of the corresponding algorithm in 2 The only differences are e This approach reduces looking at weak transitions in the new minimized system to looking at weak transitions in the original system 27 Kwon m e 33 34 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 Listing 5 11 PseudoCode for LTS minimization procedure getSplit partition splitter if partitionN splitter Z amp amp partition splitter Z Q return pi partitionN splitter Z p2 partition splitter Z Q else return false end if end procedure procedure minimizeLts states initialState var initialPartition 0 var partitions set up initial partition for each reachable state in states remove unreachable states if stateIsFullyWeakExplored state initialPartition add state else partitions add state end if end for add initialPartition to partitions if it is not empty if initialPartition length gt 0 partitions add initialPartition split partitions repeat until partitions does not change anymore for all pairs of partitions partitioni partition2 if partitioni was already split in this iteration continue for
50. ile types for example a translation from pseuCo code to Petri nets Depending on the kind of integration the pseuCo com infrastructure would need to be extended 32 1 mainAgent 4 2 3 US Minimize Expand all Random path 2 ExportLTS Random path 2 Export LTS 09 Share this file Figure 6 1 Adding additional translations doesn t scale and causes confusing UI 1 As long as the new translations are just an extension to the existing ones the current infrastructure suffices 2 There is no support for the user to select a translation chain If in addition to the old pseuCo gt CCS LTS chain a new translation chain pseuCo Petri LTS was be added the file editing interface for pseuCo files would look as illustrated in Figure 6 1 Adding such a selection capability requires changes to the editor configuration specification format in src js ui editorConfiguration js and to the controller fileEditCtr1 33 Appendix A Definitions for LTS In the following let Act be an arbitrary set with 7 Act 7 is called internal action Definition 1 LTS A Labelled Transition System LTS over Act is a triple S so where S is a set of states so S the initial state and C S x Act x S the transition relation We will write s gt t as a shorthand for s a Definition 2 For any LTS S so over Act s s S and o Act let s s b
51. imizing 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 If you view a minimized transition system click the 4 Restore button at any time to return to the original transition system Actions You can perform additional actions on the transition system using the corresponding action buttons HA Random Path Clicking this button shows a random path through the transition system You can generate new random paths by clicking Restart 3 Export LTS Clicking this button allows you to export the transition system in a number of formats You can view details about a format by selecting it in the list Please note that infinite systems cannot be exported if you try to do so the export process will get stuck Exporting large systems can take a while Some export formats fail to describe certain transition systems Please read the details before proceeding 55 pseuCo You can find information about the history of pseuCo on the landing page The following sections give you an overview over pseuCo s syntax and semantics Getting Started In pseuCo execution starts in the mainAgent mainAgent 1 execution starts here Each statement must end vvith a semicolon With println you can output strings and integer
52. ion for each prestate in state weakConnections pre poststate in transition L target weakConnections post add poststate to the set prestate weakConnections post add prestate to the set poststate weakConnections pre add if poststate and prestate have not been in these sets before add new transitions that consist of an old transition and the L newly added connection for each transition in prestate weakTransitions incoming add a longer version of transition ending in poststate to both L corresponding sets end for for each transition in poststate weakTransitions outgoing add a longer version of transition starting in prestate to both L corresponding sets end for end if end for else transition is not a tau transition for each prestate in state weakConnections pre poststate in transition L target weakConnections post add prestate to the set poststate weakConnections pre add poststate to the set prestate weakConnections post end for end if end for remember that state has been weak explored end procedure 24 1 0 This means that s t and the transition has the form s s Since s must be reachable it is either initial or has an incoming transition from a reachable state s If s is initial s s is in weakConnections by default Otherwise since s is reachable weakProcessState must have been called on it based on the breadth first order causing s S s to be added to veakConnections 2 n 0 This mea
53. ion code that provides the functionality behind a user interface and manages the data model 9 CSS a language to describe the appearance of HTML elements D3 js a JavaScript library for visualizations based on SVG elements see directive an AngularJS specific term for a HTML extension an element that provides a part of the user interface consisting of both HTML code describing the UI and JavaScript code providing the functionality factory an AngularJSispecific term for a singleton a component that provides a specific function and must be initialized once before it can be used arbitrarily often 63 Git a version control system see http git scm com grunt a JavaScript based build system see http gruntjs com jshint a tool to find common issues in JavaScript code see http jshint com node js a command line JavaScript interpreter see http nodejs org npm the Node Package Manager part of node js see https www npmjs org partial fragment of an HTML file defining a part of the UI 9 PEG js a JavaScript based parser generator to generate JavaScript parsers for arbitrary languages see PseuCoCo a compiler from pseuCo to CCS code see 64 Bibliography Sebastian Biewer A compiler for pseuCo to CCS 2013 Jaana Eloranta Minimizing the number of transitions with respect to observation equivalence BIT 31 4 576 590 1991 E Allen Emerson and Edmund M Clarke
54. ion of the minimizeLts task from worker js 739 minimizeLts function data workerState 1 740 var ltsData vorkerState dataldata dataldl 741 742 if 1tsData 743 return 744 data null 745 taskCompleted true 746 1 747 l 748 749 enhancelfNeeded 1tsData 750 751 var states ltsData core states 752 753 var initialBlock 754 var blocks 41 756 var stateToBlockMap 757 758 var notFullyWeaklyExploredStates 759 760 _ each states function state stateName 761 if contains ltsData extended explorationState explored L stateName l contains ltsData extended explorationState L frontier stateName 762 if stateIsFullyWeakExplored ltsData stateName 763 initialBlock push stateName 764 stateToBlockMaplstateNamel initialBlock 765 else 766 unexplored state 767 var newBlock stateNamel this state may not be b grouped 768 blocks push nevBlock 769 stateToBlockMaplstateNamel newBlock 770 notFullyWeaklyExploredStates push stateName 771 772 else 773 unreachable state ignore 774 775 F 776 777 if initialBlock length gt 0 blocks push initialBlock 778 779 var done false 780 781 var buildToDo function 782 var todo 783 784 each blocks function block1 785 each blocks function block2 786 todo push blocki block1 block2 block2 787 124 788 H 789 7
55. ive 7 int x chan2 now x will have value 8 Attempting to receive from an empty channel blocks the receiver attempting to send to a full channel blocks the sender Receiving is destructive Arrays come in handy for declaring multiple channels intchani00 4 chan start anAgent chan 0 chan 1 When declaring a procedure generic channel types without capacity must be used intchan5 c void p intchan c 1 p c valid procedure call Such procedures will work with any synchronous or asynchronous channel Select Case Statements 58 A case clause consists of the keyword case followed by a receive expression or a send expression a and a statement A select case statement consists of one ore more case clauses followed by an optional default clause select case chan lt a several statements in brackets case b lt chan2 or just one case lt chan3 receive and forget default always enabled Shared Memory n pseuCo several agents may share access to some variables f 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 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 data race Programs with data races are considered incorrect Explicit Locking The key
56. k amp amp L stateToBlockMap weaklyOutgoingMatchingTransition L target weakConnectionPostBlock return false L prevent tau steps from replacing themselves as L part of taux return _ some states weaklyOutgoingMatchingTransition L target weakConnections post function L stateAfter utgoingWeakMatchingTransition if oldToNewLabel b stateAfter utgoingWeakMatchingTransition L transitionToTest target return false we b ended up in the wrong state no possible b replacement we found a matching route tau gt L weaklyOutgoingMatchingTransition gt taux we still must check that this is longer than L transitionToTest otherwise each transition b would remove itself return block weakConnectionPostBlock l b transitionToTest target oldToNewLabel b weaklyOutgoingMatchingTransition target H H 5 H newStates thisBlockLabel transitions filteredUniqueOutgoingNewTransitions 3 var newInitialState oldToNewLabel ltsData core initialState add weak self loop if needed for observation congruence var blockWithInitialState stateToBlockMaplltsData core initialState b if some states ltsData core initialStatel transitions function L transition return transition weak amp amp stateToBlockMap transition target L blockWithInitialState HJ 14 newStates newInitialState transitions push target newInitialState weak true 11 var datald workerSt
57. le separate partition This ensures that states cannot be falsely considered equal because weak transitions have not been fully computed yet Consequently this means that the resulting system may not be minimal However if weak exploration finished all states start in the same partition and the result is guaranteed to be minimal The full implementation of the minimization algorithm as a background worker task can be found in Listing B 4 A simplified PseudoCode version of it is shown in Listing 5 11 To ensure the resulting system has the minimal number of transitions the algorithm must remove superfluous transitions For example in the transition system in Figure 5 9 the transition X 5 Z can be removed because X 5 Y Z and therefore X 2 2 describes an algorithm to solve this issue which removes a transition s s if there is a state 83 such that s 83 3 _ 82 V s 4 3 3 4 82 5 1 This approach only works in a transition system which is saturated meaning that s s implies s gt 82 for any states s s and for any action a PseuCo com uses an adapted version of this algorithm integrated into the construction of the new transition system To avoid having to compute the weak transitions it argues over the weak transitions in the original transition system Let LTS S so be the initial transition system Let S be the set of states of the new minimized transition system and
58. le again If it differs from the initial version that started the download process the downloaded files are assumed to be inconsistent and dropped Additionally the browser makes sure that all requests are served with old versions from the cache until the page reloads which causes an atomic switch to the new version However there is no integrated mechanism to ensure that all downloaded application files are actually fetched from the server and not from a possibly outdated cache Therefore it is important to ensure this manually by correctly setting the corresponding HTTP headers shows a suitable configuration file for It prevents all application files from being cached in the normal browser cachd and makes sure that while the application manifest may be cached the browser must check for updates on the Server on any access Remark Developing an application which uses the HTML Application Cache has a few possibly confusing differences from normal development 1 You must change the manifest for changes to be picked up by the browser 2 You must reload the page twice for changes to show up Once to trigger the update and a second time to switch to the new version 3 Depending on the HTTP server and its configuration deleting the manifest file does not stop this behaviour The application cache is cleared only if the request for the manifest results in a 404 not found error Any redirects server errors or other unexp
59. leNewStates uniq flatten map block L function stateName return _ map states stateName weakConnections post L oldToNewLabel 1 true _ each weaklyReachibleNewStates function targetStateName if targetStateName thisBlockLabel 4 targetStateName is reachable with a weak transition add that uniqueQutgoingNewTransitions push target targetStateName weak true 3 var filteredUniquetutgoingNevTransitions filter L uniqueOutgoingNewTransitions function transitionToTest check if the transition is needed or can be replaced vith L a transition of a weak post state return some blockToStateInfo block L veakConnectionPostBlocks function L weakConnectionPostBlock var veakly utgoingMatchingTransitions flatten map L veakConnectionPostBlock function L veakConnectionPostState 4 return _ filter states weakConnectionPostState L transitions function transition return transition label transitionToTest L label amp amp transition weak transitionToTest L weak 123 J true 44 945 946 949 952 953 956 957 958 959 961 962 963 964 965 966 967 968 969 970 975 985 993 994 995 weaklyOutgoingMatchingTransitions are all transitions L that might make transitionToTest superfluous return some veakly utgoingMatchingTransitions function L weaklyOutgoingMatchingTransition 4 if weaklyOutgoingMatchingTransition wea
60. lopment pseuCo com can be configured to access the server component at another URL For details see As soon as the HTTP server is running accessing it with a modern browser will open the user interface Listing 3 1 A configuration file for using as a reverse proxy RevriteEngine n RevriteRule http localhost 9128 1 P TUsing the file protocol will not work in most browsers due to security restrictions User Manual PseuCo com features an interactive user manual that can be accessed at Gaseurt help A digital printout of the manual can be found in Appendix E Remark The User Manual contains interactive elements If possible please read the online version instead of the digital printout version You can find the current public version of the user manual at http pseuco com t help 25 Developer Manual 5 1 The Debugging Page The pseuCo com UI has a hidden debugging page that allows quick access to some internal settings located at 5 2 Dependencies PseuCo com depends on several JavaScript libraries both for the build system and for the actual application Libraries are managed by and A full list of libraries can be found in the corresponding configuration files Listing 5 1 shows all dependencies that Bower installs which are runtime dependencies Similarly Listing 5 2 shows the dependencies installed by npm All of them are build time dependencies except for Th
61. lowing minimization to be run on it For any state all weak transitions must have been found if weak exploration has run far enough that all paths starting in this state must pass at least two non 7 transitions before reaching a state that has not been visited by weak exploration yet Whether this is the case can be determined by the algorithm given in Listing B 3 a PseudoCode version is given in Listing 5 10 If this algorithm returns true the sets weakConnections and weakTransitions will not be changed further during weak exploration PseuCo com makes direct use of this property As soon as the user requests the minimization result weak exploration is paused and the system enters the partitioning phase While the resulting system may not be minimal this ensures a prompt response to the user s request since weak exploration has the highest computational cost in the minimization algorithm 5 11 2 Partitioning Transition Minimization amp Generation of the Resulting System The actual partitioning is similar to the algorithm in 4 an alternative description of which can be found as the naive version of the relational coarsest partitioning algorithm in 5 There is one key difference Initially not all states start in one partition Instead states which are not fully weakly explored as 26 explained in subsection 5 11 1 are placed in a separate one state partition each while all fully weakly explored states start in a sing
62. lying foundational objects This resulted in the open source software available at https github com Biever PseuCoCo It also contains a parser and type checker for pseuCo in JavaScript written by Pascal Held However contains no full graphical user interface and there are no ways to interact with the resulting transition system except for a simple tracing functionality 2 4 Explanation of Symbols and Technical Terms refers to the path where you stored the source code repository of pseuCo com In the electronic version you can click on the remainder of the path to see the current version in the public online repository refers to the URL where you access pseuCo com either http pseuco com or the URL your local webserver runs at In the electronic version you can click on the remainder of the path to see the online version at http pseuco com refers to the path where the pseuCo com server component can be reached For the public instance this is http pseuco com api e A short description of some technical terms can be found in the glossary on page 64 e U P Accessing pseuCo com To access pseuCo com you can either use the public online version or build it from source yourself 3 1 Accessing the Online Version of pseuCo com Using a modern webbrowser open http pseuco com Given a working internet connection this will open the application and save a copy for later offline use In the future
63. nfiguration file for grunt 1 module exports function grunt 2 useustricot 3 4 var aceVersion 1 1 7 6 grunt initConfig 7 pkg grunt file readJSON package json 8 curl 9 ace 10 src https github com ajaxorg ace builds archive v aceVersion b zip 11 dest managed components ace ace 4 aceVersion zip 12 L 13 1 14 unzip 15 ace 16 src managed components ace ace aceVersion zip 17 dest managed components ace build 18 router function filepath 19 return filepath split splice 1 join 20 21 22 23 bower 24 install 25 options 26 targetDir managed components bover 27 cleanTargetDir true 28 J 29 J 30 1 31 uglify 32 options 33 mangle false 34 sourceMap true 35 1 36 app 1 37 files 38 gt temporary_files build js app min js temporary_files build js app b sgqe 39 40 r 41 lib 42 files 43 temporary files build js lib min js temporary_files build js lib b age 44 Y 45 r 46 worker 47 files 1 35 48 49 50 l 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 temporary files build js worker min js temporary_files build js L worker js Y J r concat app 1 src e
64. ns that the chain s 3 s gt s s 4 t contains at least one intermediate state We know that veakProcessState must be called on s s s2 54 1 since they are all reachable s is reachable by assumption all others are because they are reachable from s Let s be the one where weakProcessState is called last and s be the next one in the chain We know that weakProcessState has been called on all other states Since the weak transitions s sf and s 5 t are based on chains shorter than n we know by induction they already must have been added to the corresponding weakConnections sets Then weakProcessState must find s t during its search and add it All cases have been considered a Lemma 2 The sets in weakTransitions are computed correctly as specified in subsection 5 11 1 Proof Soundness can be shown by induction over the program execution The initial state no weak transitions is sound Whenever any transition s t is added to weakTransitions it is caused by any of the following combinations e 55 s D s S d esSs t e 5 5 s St All of these must be valid by induction and cause s t to be a valid weak transition by definition For completeness we need to show that every weak transition s S t with a Z r is actually added to weakTransitions during weak exploration if s and t are both reachable This is shown similarly as in the proof of by induction on the length of the chain of transitions s 4
65. nts managed by contains all files from the dependencies shown in List vw vw Ww Ing build contains the resulting directory structure the web server should present see Appendix D managed_components contains files managed automatically by the build scripts fl ace contains the downloaded archive and unzipped version of fg bower contains only the needed files from the Bower dependencies shown in node modules managed by npm contains all files from the dependencies shown in Listing 5 2 server contains the files needed for the server component see y data the data directory for the server component fg paste files that have been submitted to the paste service from users y templates template files that will be offered to users separated by file type B ccs json B its json B pseuco json Bi server htaccess configuration file for pache to direct incoming HTTP req 1ests to the 8 8 pseuCo com server running at port 9128 b B server is the server code src ar css all CSS files needed by pseuCo com CSS definitions can be in any CSS file in this folder the separation in different files is purely for convenience fg ing contains images used in pseuCo com fl js contains all main JavaScript files fig partials contains partials htaccess configuration file for Apache setting headers to disable the normal client side caching in favour of t
66. ons Without a sound understanding of how AngularJS works most of the code of pseuCo com will be hard to understand The website of ngularJS has some small examples demonstrating the way AngularJS applications work as well as many useful resources in the Learn tab in most AngularJS applications the application start up is controlled by the main HTML file The core part of it is shown in Listing 5 3 ROM Listing 5 3 Simplified and shortened version of index html lt DOCTYPE html lt html lang en data ng app cp app manifest offline appcache gt lt head gt lt meta name viewport content user scalable no width device width initial L scale 1 maximum scale 1 lt head gt lt body gt lt div class navbar navbar inverse navbar fixed top role navigation data bs L navbar gt navigation bar elements gt lt div gt lt div class fill id mainFill gt lt div class container fluid id mainContainer gt lt div data ng view id view gt lt div gt lt div gt lt div gt lt script src js lib min js gt lt script gt lt script src js app js gt lt script gt lt body gt lt html gt Listing 5 4 Simplified and shortened route configuration from app js config function routeProvider routeProvider when landing 4 templateUrl partials landing html 3 when files controller filesCtrl templateUrl partial
67. ow rigin 2 When a client sends an OPTIONS request the server responds with Access Control Allow Methods GET POST Access Control Max Age 3600 and mirrors all values listed in the Access Control Request Headers header of the request in the Access Control Allow Headers header of its response This indicates to the client s browser that it is allowed to send arbitrary GET and POST requests 5 13 A Build Server for pseuCo com PseuCo com can be built on a remote server usually on the server that hosts the repository and serves the resulting page publicly The exemplary script in Listing 5 12 automates this process It accepts the branch to build as its single command line argument and performs the following actions 1 If the branch specified is master which contains the public server part stop the server 2 Check out the specified branch from the Git repository 3 Install missing npm packages and remove superfluous ones see http www w3 org TR access control 30 Listing 5 12 A build script for server side building bin bash GIT REPO HOME repositories concurrent programming web git CHECKOUT DIR var www virtual fefrei apps concurrent programming web 1 echo Building branch 1 echo Preparing mkdir p CHECKOUT DIR o O amp om i0 if 1 master 11 then 12 echo Stopping server 13 Svc d home fefrei service cpw server 14 fi 16 echo Checking out i7 GIT W
68. p S S a function mapping old states to the corresponding new states For any weak transition s s in the old transition system 81 p si and s are computed and the corresponding transition s s is added to the transition system unless any of the following conditions hold 1 a T p si p sa This prevents 7 self loops from being added to the result 2 There are Sq sp Sc Sa such that all of the following conditions hold a Sq Sh se gt Sa b 2 sa sl c a r p sp p sc d p sa s e p sa Z p sv V p sc Z psa This condition describes the same idea as Equation 5 1 but is easier to compute It only reasons over weak transitions in the original system which have already been computed for the minimization Condition 2a ensures that the states build a path as in Equation 5 1 Condition Bb ensures that the starting state s actually corresponds to the correct starting state in the minimized system Condition belarus that s gt s does not correspond to a 7 self loop in the new system which could be removed Condition Bd ensures that the ending state corresponds to the correct ending state in the new system Finally condition 2e ensures that either s s or Se sa or both correspond to an actual 7 step in the minimized LTS While in pseuCo com weak transitions do not have to be fully computed to start a minimization leaving out weak transitions can only make t
69. r supporting the application cache because the configuration file is referenced in index html as shown in Listing 5 3 Additionally this configuration file defines tz TEL api to be a NETWORK path This ensures that the path is not cached since it is used to communicate with the server component Furthermore it prevents the browser from blocking access to it based on a rule in the HTML Application Cache specification that tries to ensure applications behave the same in online and offline mode While this suffices to ensure pseuCo com works offline there are subtle details which make updates work properly As soon as the application cache received and stored a complete copy of the application the server will never be contacted again except for two possible reasons To access a NETWORK path or to update the manifest file When the application is updated the manifest file must change too to ensure that existing users download the new version To achieve this the build process not only copies the manifest to the output directory but appends the build date as a comment to the file as shown in the copy appcache section of Listing B 1 see https html spec whatwg org multipage browsers htmlfoffline 3index html is not listed here since the index file is included implicitly 10 x O 6 G P property type effect fullName string the human readable name of the file type allowCreation boolean if enabled show
70. removed if there are states 53 54 such that s s3 s4 82 Correctness follows by saturation s 4 gt s4 implies 54 54 allowing the transition to be removed based on the first disjunct in Equation 5 1 To ensure the result is observation congruent in addition to being weakly bisimilar a 7 self loop is added to the new initial state if and only if the initial system contained a strong 7 transition from its initial state to another state which ends up in the partition that contains the initial state 5 12 The Server Component of pseuCo com PseuCo com mostly is a JavaScript application running client side in the browser This only requires a HTTP server to deliver the static application files However there are two features that use an active server component 1 To create new files users can choose start with template files that can be updated without updating the whole application 2 Users can create short links to files Opening such a link opens the pseuCo com user interface and directly navigates to the file that was shared By default pseuCo com communicates with the server at Ezscvzz api The server is implemented to listen at port 9128 and configures to forward the requests to to this port acting as a reverse proxy The server is implemented in JavaScript and designed to be run with node js All server code is located in The server implements the following API calls 1 Exzrssse vgU p
71. ro is libs d6 gt src js app js erc js ui ui j s gt src js files files js src js actions actions js gt src js tasks tasks js arc js api api js aro js tools tools js src js js gt src js pre pseucoco js helper for browserify build BIlsrc js post pseucoco js helper for browserify build PIlsrc js pseucoco js must be build with brovserify lsrc js worker js must be executed as Web Worker BIsrc js tasks backgroundWorker js must be executed as Web Worker l dest temporary files build js app js nonull true options stripBanners true banner 1lu 0licenseu c uCopyrightu2014uFelixuFreiberger Containsu L PseuCoCo u c Copyright 2013 2014 Sebastian Biewer Detailsyiny L ReadMe mdyjoryjon the About tab n Y lib src gt managed_components bower jquery jquery js gt managed_components bower angular angular js gt managed_components bower js managed components ace build src ace is l dest temporary files build js lib js nonull true Y CCS 1 src temporary files CCSParser is temporary files CCS no parser is l dest temporary files CC js nonull true Y PseuCo 1 src temporary files PseuCoParser is temporary files PseuCo no parser is 1 dest temporary files PseuCo is nonull true worker src gt src js pre pseucoco js gt temporary_files pseucoco js
72. rom the normal cache Here is how you can do that in some modern browsers Browser Steps Chrome open the URL chrome appcache internals find this application Remove Firefox Menu button Options Advanced Network find the application in the list on the bottom Remove nternet Gear icon Internet Options Settings in the section Browsing history Explorer Caches and databases find the application in the list gt Delete Safarion Settings Safari Advanced Website Data find the application in the iOS list on the bottom Edit Delete icon Delete 62 Glossary Ace a JavaScript based text editor see http ace c9 10 AngularJS a rich JavaScript framework that helps building dynamic HTML based applications by enhancing HTML see https angularjs org B 9 3 75 63 Apache a HTTP server see B zier curve a curved described by several usually four so called control points defining not only the start and end point but also points the curve will bend towards see https en wikipedia org wiki Bf Bower a package manager for web applications see Browserify a JavaScript tool to bundle JavaScript files with their apm dependencies to be runnable in a browser environment see http browserify org CoffeeScript a programming language that cross compiles to JavaScript see http coffeescript org controller refers to applicat
73. ructures that can encapsulate data It is also possible to define procedures in them which usually operate on the encapsulated data Only methods are accessible from outside the structure struct Count int a 0 int plusPlus a return a Instances of a structure are declared just like variables but using the name of the structure The available methods can then be accessed using the notation Count s println s plusPlus Call By Value Call By Reference When evaluating procedure calls arguments with one of the primitive types bool int and string are initialized with copies of the passed value Call By Value 57 For arrays struct monitor mutex and channels a reference to the same object is used Call By Reference void p int i int 1 a i 42 a 0 1337 mainAgent int i int 1 a println i a 0 prints 0 1337 Message Passing PseuCo features channels for communication between agents Channels Channels can be synchronous or asynchronous and have any of the primitive types bool int Or string Asynchronous channels are declared with a fixed capacity boolchan chani synchronous type bool intchan7 chan1 asynchronous type int 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 intchan7 chan2 chan2 7 send 7 chan2 8 and send 8 chan2 rece
74. s 361 var stateIsWeakExplored function ltsData stateName true if a state has been L weak explored 362 return ltsData core states stateName weakExplored 363 3 364 365 366 var stateIsWeakConnectionExplored function ltsData stateName if true no L more states will be added to weakConnections 367 var state ltsData core states stateName 368 if state weakConnectionExplored return true 369 370 if stateIsWeakExplored ltsData stateName amp amp every state weakConnections post L function postStateName 371 return stateIsWeakExplored ltsData postStateName 372 100 373 state weakConnectionExplored true 374 return true 375 else i 376 return false 377 378 F 379 380 381 var stateIsFullyWeakExplored function ltsData stateName if true no more b weak transitions or connections will be added to this state 382 var states ltsData core states 383 var state states stateName 384 385 if ltsData extended explorationState explorationFinished return true 386 if state fullyWeakExplored return true 387 if statelsWeakConnectionExplored ltsData stateName return false 388 389 if every state weakTransitions outgoing function transition 390 return stateIsWeakConnectionExplored ltsData transition target 391 J 392 state fullyWeakExplored true 393 return true 394 J 395 396 return false 397 3 Listing B 4 Task funct
75. s files html ZZ othervise redirectTo After loading the library and application code which just defines the components but does nof actually erecute any application code processes the HTML elements The attribute data ng app cp app on the lt html gt element causes the module cp app to be loaded which is de fined in This sets up some shared data but most importantly it configures routeProvider as shown in This causes to read the route in the URL load the corresponding and inject the corresponding into div data ng view id view gt lt div gt For example if the user opens the is injected and filesCtrl defined in z rc js ui controllers filesCtrl s is instantiated 5 5 How pseuCo com Stores and Handles Files In pseuCo com users can create and store files These files are stored in the user s browser using the HTML Web Storage File storage is managed by the factory files in the module cp files the definition of which can be found in ksessnes l src 1s files files s It uses the angularLocalStorage library Upon creation every file is assigned a random 12 digit id by which it can be referred to later on To allow listing all files without storing the data of all files in a single key slowing down access file metadata is stored separately from file contents There is a single repository of file metadata stored under lsee http www whatwg or
76. ses Consequently there are many tools to create view and analyse such systems However many of these tools are hard to set up or use or cannot work with large or infinite transition systems This unnecessarily complicates the use of such systems especially for teaching There complex set up cannot be expected from students and infinite systems are regularly analysed while exploring the limits of LTS and languages having LTS semantics For this thesis a new application handling labelled transition systems was developed pseuCo com Being a JavaScript based web application it offers a set up free experience while still keeping many advantages of classic native applications like offline use In addition pseuCo com was designed to work with large or infinite transition systems as well as with small ones enabling users to view and analyse them just as they would expect Users can visualize any transition system right in their browser with the ability to expand and collapse states as they wish While automatic graph layout keeps the system easily readable even as states appear and disappear users are free to rearrange states as they wish Support for partial minimization even of infinite systems allows to get a faster overview over the behaviour modelled by a system PseuCo com includes a compiler from pseuCo to CCS and a mechanism to convert CCS terms to labelled transition systems Both are based on PseuCoCo 1 and seamlessly
77. specified when a task is submitted 5 7 2 Defining a Worker To define a worker you need to build a JavaScript file containing everything the worker needs to execute and place it at any path accessible to the application preferably js worker js relative to the base path of your application This file must contain in the following order 1 all library code that the worker needs 2 a definition of the variable workerData as specified below see https html spec whatwg org multipage workers htmlitworkers 13 3 a verbatim copy of the file src js tasks backgroundWorker js You can define multiple types of workers in one file They are distinguished by a name called type Each worker has one object storing its state This object will be passed as workerState to all functions that may access it The workerData variable must be an object Each property of this object defines a worker type given by the property s key The value of each such property must be an object with two properties An initialization function initialize which will receive workerState as its argument and may create arbitrary properties in the workerState object and an object tasks For each task the worker can carry out tasks must contain a property whose key is the task name and whose value is a function the task function Each task function receives two arguments data and workerState The data is provided by the caller and workerState is the objec
78. t discussed above The task function must return an object with at least the following two properties A boolean value taskCompleted and a serializable object data Each time a task function returns data will be sent to the caller If taskCompleted is false the task will be scheduled to execute again If the return value contains a property newPriority containing a number the task s priority will be modified to match that number A task function is free to modify the data object to store intermediate results To ensure that the worker has a chance to process other tasks with a higher priority or detect that a task has been cancelled task functions should regularly return intermediate results if amy and taskCompleted false waiting to be called again by the framework You can find an example of a worker definition in Ezessesy src js worker js 5 7 3 Using a Worker To use a worker developers can use the API given by the factory taskManager It offers the following methods e getRunningTaskCount is a zero argument function that returns the number of tasks in the execution queue e requestWorker type crashCallback sourcePath is a function that starts a worker type is a string indicating the type the worker should have as specified in the worker definition crashCallback error is a function that will be called when the worker encounters an uncaught exception Remark Do not use this mechanism for expected exceptions
79. tate ltsData core states transition target 320 insertConnection targetState weakConnections pre transition target 321 insertConnection targetState weakConnections post transition target 322 323 if transition veak 324 veak transition 325 326 update veak connections 327 _ each state weakConnections pre function preStateName 328 each targetState veakConnections post function postStateName 4 329 var vasNev insertConnection states preStateName L veakConnections post postStateName 330 insertConnection stateslpostStateNamel veakConnections pre L preStateName 331 332 if wasNew 1 333 we discovered a new connection 334 this might allow new transitions longer than existing b ones 335 336 each states preStateName weakTransitions incoming L function t 1 337 createTransition t source postStateName t label 338 H 339 _ each states postStateName weakTransitions outgoing L function t 4 340 createTransition preStateName t target t label 341 335 342 343 H 344 H 345 else 346 strong transition 347 348 create weak transitions 40 349 each state weakConnections pre function preStateName 4 350 each targetState weakConnections post function postStateName 4 351 createTransition preStateName postStateName transition label 352 H 353 30 355 y 357 state weakExplored true Listing B 3 stateIsFullyWeakExplored and utility functions from worker j
80. te or touch the state to show the label in the grey tool bar on the bottom 54 Other Modes for Exploring LTS Graphs For large graphs there are alternative modes to help you retain control They can be enabled by ticking the appropriate checkboxes on the grey tool bar or in the settings panel you can reveal by clicking the tool bar 2 Pin dragged nodes helps you to arrange complex graphs if the automatic arrangement produces unacceptable results If you enable this option any state you drag will stick to the position where you dropped it To release a state disable this option and drag the state again Focus on single node helps you by automatically collapsing nodes With this setting enabled only one state can be expanded fully all other states will collapse to only show you the paths leading to the focused state Additional Display Options Clicking the grey tool bar reveals a panel with additional options It allows you to Compress weak steps to save space Weak transitions will be shorter and have no visible label Export as SVG graphic This will show SVG code Copy it and save it to an empty text file and save it with the file extension svg to get a vector graphic export of the current LTS view LTS Minimization For any transition system pseuCom com can compute the minimal observation congruent transition system for you Start this process by clicking the X Minimize button in the tool bar Fully min
81. th as few distractions as possible click the maximize icon in the navigation bar The UI will shrink hiding elements that are less important Hint You can also enable full screen mode in your browser On desktop browsers this usually happens when you press F11 or 3F To leave this mode click the restore icon in the top right corner The mode will also be disabled automatically when you navigate to another page File Types Labelled Transition Systems LTS graphs can be huge so pseuCo com cannot display them completely Therefore you can interactively expand just the parts of the graph you are interested in When you see a new LTS graph you will only be shown the initial state If you click on this state it will expand revealing all successor states The color of a state will turn into a lighter red to tell you that this state is fully expanded If a state turns blue it is terminal meaning that there are no successors To save space you can collapse nodes you are 2 Minimize Collapse all no longer interested in by clicking on them Try it right here This is interactive The application tries to show you LTS graphs as clearly arranged as possible but this may not always work automatically If the graph gets tangled up you can drag the nodes to rearrange them Labels for states will be show on the states themselves only if they are extremely short Otherwise hover your mouse over a sta
82. tion systems computing the smallest transition system that still is observation congruent see Definition 6 to the original transition system There are many well known minimization algorithms 2 4 b but they assume to be run on fully explored transition systems PseuCo com however has the goal to provide users with tools that work as far as possible with extremely large or even infinite transition systems requiring modification to he classic approach The design goals of such a minimization feature are e If the system is fully explored return the unique 2 minimal observation congruent system 19 Figure 5 5 A result of graph layout with control nodes extinguish extinguish Figure 5 6 Graph layout with control nodes sometime produces bad results 20 e If the system is not fully explored provide a safe approximation of the minimal system If in doubt assume states cannot be unified e Pre compute all data that would be needed for full minimization so it can be used if the user requests minimization before exploration finishes The resulting algorithm is highly similar to the one described in 2 and works in four distinct phases 1 Weak transitions are computed 2 The relational coarsest partitioning is computed using the algorithm from 4 Since weak transitions have been added to the transition system the result is weakly bisimilar 2 3 The algorithm from 2 to minimize the number of transi
83. tions is run 4 To ensure observation congruence a 7 self loop is added to the initial state if necessary However the actual algorithm contains subtle differences to this simplified version to cope with partially unexplored systems and to increase performance The details are given in the following sections 5 11 1 Computing Weak Transitions The minimization algorithm needs access to the weak transitions in the transition system They are pre computed by an exploration mechanism weak exploration similar to the mechanism described in section 5 9 Weak exploration runs in parallel to the normal exploration but is slightly delayed This ensures that a user can quickly see the initial fragment of the transition system but as soon as exploration got ahead of the user weak transitions are computed as fast as possible to allow minimization to run The core function of this algorithm weakProcessState is called automatically in a breadth first manner by the exploration mechanism its only remaining responsibility is to update the weak transition information to incorporate the transitions starting in the state it processes To allow for a simpler and faster implementation weak r transitions are stored as weakConnections separate from all other transitions which are stored in veakTransitions In both cases transitions are stored in both their start and end state Let LTS S so be a transition system and Sreach be the s
84. values println 7 println 7 4 Primzahl You can declare variables locally or globally Initialization is optional int x 5 mainAgent bool y defaults to false y true x 4 Variables may be declared at most once Procedure definitions need a return value and types for all arguments int calculateSomething int inputl bool input2 do something return 5 Procedures that do not return anything have the return type void Expressions Conditionals and Loops A conditional looks like this if condition then case else else case The else case is optional In conditions the operators negation equality test amp amp logical and and logical or are supported 56 There is also an in line conditional expression println n 5 viel wenig Both while and for loops are available while expression repeats until the condition is false for initializer condition caction repeats until the condition is false Agents Agents can be declared vvith the agent keyvvord agent a1 calculateSometing input1 input2 start al start calculateSomething input1 input2 anonymous agent Agents do not need to be started immediately when they are declared and may be anonymous If an agent is not waiting for its termination is achieved by the join keyword join a1 Structures The struct keyword allows declaring st
85. ver when the share was created b temporary true will be given for temporary shares Otherwise this property is omitted 3 fAFLLazUmL templates get allows to get access to the templates that are stored on the server for a specific file type Requests to this path must be GET requests and have a single parameter type a string representing the file type for which the templates are requested The server will return a JSON object having an array templates as its single property It is an array of templates each being an object having the following properties a name is a name for the template b description is a description string for the template which may contain basic HTML formatting including links c content is the content of the template If the user selects the template content should be used to initialize the contents of the file that is created The server features a banning system to prevent malicious users from causing excessive system load on the server The server sets Cache Control headers to ensure that the responses it gives may not be cached except for successful calls to Ixersssevguj paste get Since the clients interacting with this server are sandboxed inside browsers the server has to conform to the Cross Origin Resource Sharing standard to ensure clients are allovved access to it 1 To ensure not just clients running in the same domain can access the server it sends the header Access Control All
86. w satisfied using signal or signalAll 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 monitor Count int i condition notNull with i gt gt 0 void inc i now someone can do a dec signal notNull void dec waitForCondition notNull i CCS CCS is a process calculus to model concurrent systems PseuCo com uses a pragmatic extension of CCS with value passing sequencing and termination If P and Q are valid CCS processes then the following are valid CCS processes as well Process Semantics 0 cannot perform any action 1 terminated process emits behaves like e afterwards a P performs action a behaves like P afterwards P Q non deterministic choice between P and Q 60 P Q concurrent execution of P and Q P N a b c behaves like P except that actions a b c are not allowed P N a b c behaves like P except that only actions a b c are allowed P Q behaves like P until it terminates then performs a r transition to Q X behaves like P if X was defined before as X P A CCS action is any combination of letters starting with a lower case letter Some of them have a special meaning Input Sequence Action Meaning i T tau represents in internal non observable action e delta signals that a process has terminated CCS actions ma
87. word mutex is used to declare a lock or mutex Locks are used to coordinate access to data by preventing concurrent access preventing data races Locks can be locked with 1ock and unlocked with unlock mutuex m declaration int i 5 void dec lock m give it to me i no data race unlock m done 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 Implicit Locking The keyword monitor instead of struct declares a monitor a structure that makes use of an implicit lock There is a built in mechanism that locks this lock before any monitor method call is effectuated and unlocks it only after the method s return has happened This ensures that the encapsulated data is properly guarded against data races 59 monitor Count int a 0 int plusPlus a return a Monitor methods may need to wait for specific conditions concerning the data encapsulated by the monitor before effectuating certain operations on them Conditions are declared with the keyword condition The waiting is done by waitForCondition 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 no
88. y contain a or If both counterparts can be executed at the same time they can synchronize resulting in an internal r transition After a sending expression can be given the value of which will be bound to the input variable given after Input variables may be bound to a range defined as range R 0 0 with R Ranges of string length can be specified too allows strings of length 1 to 3 A process name is any combination of letters starting with an upper case letter Process definitions may contain an arbitrary number of variables in square brackets which must be given when a process is called To get examples for valid CCS terms create a new CCS file and select a template Offline Mode The application is available offline automatically if supported by your browser Just reopen pseuCo com http pseuco com to access it Frequently Asked Questions My LTS graph shows only one state but I m sure there must be some transitions The graph is not shown automatically since graphs can be too huge to render in a readable way Click on a state to expand it and you will see all successors of the state Click here for more information In the LTS graph l can see the states but transitions aren t drawn completely 1 just see their label text but no arrow 61 You re using Internet Explorer right This is a known bug that Microsoft has not fixed yet Please tell Microsoft you can reproduce this bug here
89. you can open this URL even without an internet connection to use the saved copy 3 2 Building pseuCo com from Source The source code of pseuCo com can be acquired using Git from its public repository which is located at http git fefrei de concurrent programming web git PseuCo com has many build and run time dependencies most of which can be installed automatically However some have to be installed manually upfront 1 a recent version of node js from http nodejs org including npm the Node Package Manager 2 the command line interface of grunt cli which can be installed by running npm install g grunt cli All other dependencies can be installed by npm and the default build script If git node and grunt cli are installed correctly you can fetch and build pseuCo com as follows git clone http git fefrei de concurrent programming veb git cd concurrent programming veb npm install grunt For file sharing and file templates pseuCo com needs a server component While being in the directory server it can be run with node server js The server will run on port 9128 To open the directory Fer build needs to be served by an HTTP server By default pseuCo tries to reach the pseuCo com server at relative to the URL it is running from A reverse proxy can be used to forward request to this URL to the server component as shown in Listing 3 1 Alternatively for deve

Interactive Visualization and Minimization of

Contents

Download Pdf Manuals

Related Search

Related Contents