https://wiki.eecs.umich.edu/desuma/index.php?title=Special:Contributions/Yuweibao&feed=atom&deletedOnly=&limit=50&target=Yuweibao&topOnly=&year=&month=DESUMA Wiki - User contributions [en]2022-08-17T17:37:15ZFrom DESUMA WikiMediaWiki 1.17.0https://wiki.eecs.umich.edu/desuma/index.php/DESUMADESUMA2017-08-22T20:43:58Z<p>Yuweibao: /* Input Reference */</p>
<hr />
<div>== DESUMA Software ==<br />
[[File:DESUMA1.png|400px|thumb|right|DESUMA 1.5.4 interface for Windows]]<br />
The Discrete Event System, University of Michigan and Mount Allison University, or DESUMA, is a software and educational tool used to build, analyze and control models of Discrete Event Systems (DES) as finite-state automata (FSA). It consists of the integration between the UMDES library (a set of commands for DES operations), developed at the University of Michigan under [http://web.eecs.umich.edu/~stephane/ Prof. Stephane Lafortune], and the graphical environment for visualizing discrete event systems, called GIDDES (Graphical Interface for the Design of Discrete Event Systems), developed at Mount Allison University under [http://www.mta.ca/~lricker/ Prof. Laurie Ricker]. DESUMA allows the user to perform a variety of manipulations of discrete event systems modeled by FSA related to model-building, fault diagnosis, verification, control under full and partial observation, and decentralized control.<br />
<br />
Continuous development of DESUMA is a joint effort between Mount Allison University (Prof. Ricker and her colleagues) and University of Michigan (Prof. Lafortune and his colleagues).<br />
<br />
'''Note:''' UMDES commands are embedded within the DESUMA software. However, running commands from the command line is also possible. See UMDES section for more.<br />
<br />
<br />
== DESUMA2 ==<br />
[[File:DESUMA2.png|400px|thumb|right|DESUMA 2.0.0 interface for Windows]]<br />
DESUMA2 is the latest software version made public in 2014. Notable changes from the previous DESUMA version include the FSA layout being done using J-Graph instead of GraphViz due to compatibility problems with the latest JAVA versions. Several GUI related enhancements were made, and known bugs in the underlying UMDES commands were fixed.<br />
<br />
== DESUMA Resources ==<br />
<br />
=== Tutorial ===<br />
:Please visit [[Getting Started with DESUMA2]] for information on using DESUMA2 and its interface.<br />
<br />
:Visit [[DESUMA2 Functions]] for information on the UMDES menu within DESUMA2.<br />
<br />
=== DESUMA Software Download ===<br />
:Click this [https://www.eecs.umich.edu/umdes/projects/lib/download_access/submit_desuma.html link] to download the latest and/or older versions of DESUMA<br />
<br />
:Visit [[DESUMA Installation Instructions]] for proper step by step procedures of installation.<br />
<br />
<br />
== UMDES ==<br />
<br />
UMDES is a library of routines, written in C, for creating and manipulating discrete event systems modeled as FSA. In particular, many of the algorithms for the theory of supervisory control and from the theory of diagnosability of DES are implemented in UMDES. While the main commands in UMDES are embedded within DESUMA, users are still able to run these commands from the command line. For this reason, compiled UMDES commands are available for download.<br />
<br />
'''Note:''' A slight source of confusion is that the names of the UMDES executables do not always exactly match the names of the same commands in DESUMA and DESUMA2 menus for UMDES.<br />
<br />
<br />
=== UMDES Resource ===<br />
<br />
Please go to the [[UMDES Software Library]] page for more information on downloading and using UMDES separately from DESUMA and DESUMA2.<br />
<br />
<br />
== UMDES21 ==<br />
<br />
UMDES21 is a library of routines, written in java, for verifying the opacity of discrete event systems modeled as FSA. In particular, current-state opacity, initial-state opacity, infinite-step opacity, and K-step opacity verification are implemented in UMDES21. The main commands in UMDES21 are embedded within DESUMA, and users are able to run these commands under the UMDES21 menu in DESUMA.<br />
<br />
=== Input Reference ===<br />
<br />
'''Current State Opacity Verifier'''<br />
<br />
:Input: <br />
:1) A graph to perform current-state opacity test on<br />
<br />
::Format: .fsm<br />
<br />
:2) A state data file: a file that lists the names of all the secret states<br />
<br />
::Format: .states<br />
<br />
:Output: <br />
:1) "This fsm obeys current-state opacity"<br />
<br />
:2) "This fsm violates current-state opacity"<br />
<br />
::"The violating states (in the observer) are…”<br />
<br />
<br />
<br />
'''Initial State Opacity Verifier'''<br />
<br />
:Input:<br />
<br />
:1) A graph to perform initial-state opacity test on<br />
<br />
::Format: .fsm<br />
<br />
:2) An initial state data file: a file that lists the names of all the initial states, and their secrecy status<br />
<br />
::Format: .init<br />
<br />
:Output:<br />
<br />
:1) "This fsm obeys initial-state opacity"<br />
<br />
:2) "This fsm violates initial-state opacity", <br />
<br />
::"The violating states (in the observer of the reversed automaton) are…”<br />
<br />
<br />
<br />
'''Infinite/K-Step Opacity Verifier'''<br />
<br />
:Input: <br />
:1) A graph to perform infinite/K-step opacity test on<br />
<br />
::Format: .fsm<br />
<br />
:2) A state data file: a file that lists the names of all the secret states<br />
<br />
::Format: .states<br />
<br />
:3) K value: infinite step(any input K<0), K-step(the specific value K>=0)<br />
<br />
::Format: integer<br />
<br />
:4) Ultra fast mode: no Two-Way Observer generated; or<br />
<br />
::Fast mode: Two-Way Observer generated<br />
<br />
:Output:<br />
<br />
:1) "This fsm obeys infinite/K step opacity"<br />
<br />
:2) "This fsm violates infinite/K step opacity", <br />
<br />
::"The violating states (in the Two-Way Observer) are…”<br />
<br />
:3) If “Fast Mode” is chosen, the Two-Way Observer will be generated in .fsm format under the directory /temp.<br />
<br />
=== Format Reference ===<br />
1) '''.fsm'''<br />
<br />
:Line1: <#of states><br />
<br />
:Line2: <state name> <marked? 1(Y):0(N)> <#of transitions><br />
<br />
:Line3: <event name> <next state name> <observable? o(Y):uo(N)><br />
<br />
:…<br />
<br />
'''Example:'''<br />
<br />
:4<br />
<br />
:state0 0 2<br />
<br />
:uo state1 uo<br />
<br />
:uo state2 uo<br />
<br />
<br />
:state1 0 2<br />
<br />
:a state3 o<br />
<br />
<br />
:state2 0 1<br />
<br />
:b state1 o<br />
<br />
<br />
:state3 1 1<br />
<br />
:a state2 o<br />
<br />
<br />
<br />
2) '''.states'''<br />
<br />
:Line1: <secret state name1><br />
<br />
:Line2: <secret state name2><br />
<br />
:…<br />
<br />
<br />
'''Example:'''<br />
<br />
:state4<br />
<br />
:state2<br />
<br />
<br />
<br />
3) '''.init'''<br />
<br />
:Line1: <initial state name1> <secret? 1(Y):0(N)><br />
<br />
:Line2: <initial state name2> <secret? 1(Y):0(N)><br />
<br />
:…<br />
<br />
<br />
'''Example:'''<br />
<br />
:state2 1<br />
<br />
:state3 0<br />
<br />
:state0 1</div>Yuweibaohttps://wiki.eecs.umich.edu/desuma/index.php/DESUMADESUMA2017-08-22T20:43:20Z<p>Yuweibao: UMDES21 input output specification</p>
<hr />
<div>== DESUMA Software ==<br />
[[File:DESUMA1.png|400px|thumb|right|DESUMA 1.5.4 interface for Windows]]<br />
The Discrete Event System, University of Michigan and Mount Allison University, or DESUMA, is a software and educational tool used to build, analyze and control models of Discrete Event Systems (DES) as finite-state automata (FSA). It consists of the integration between the UMDES library (a set of commands for DES operations), developed at the University of Michigan under [http://web.eecs.umich.edu/~stephane/ Prof. Stephane Lafortune], and the graphical environment for visualizing discrete event systems, called GIDDES (Graphical Interface for the Design of Discrete Event Systems), developed at Mount Allison University under [http://www.mta.ca/~lricker/ Prof. Laurie Ricker]. DESUMA allows the user to perform a variety of manipulations of discrete event systems modeled by FSA related to model-building, fault diagnosis, verification, control under full and partial observation, and decentralized control.<br />
<br />
Continuous development of DESUMA is a joint effort between Mount Allison University (Prof. Ricker and her colleagues) and University of Michigan (Prof. Lafortune and his colleagues).<br />
<br />
'''Note:''' UMDES commands are embedded within the DESUMA software. However, running commands from the command line is also possible. See UMDES section for more.<br />
<br />
<br />
== DESUMA2 ==<br />
[[File:DESUMA2.png|400px|thumb|right|DESUMA 2.0.0 interface for Windows]]<br />
DESUMA2 is the latest software version made public in 2014. Notable changes from the previous DESUMA version include the FSA layout being done using J-Graph instead of GraphViz due to compatibility problems with the latest JAVA versions. Several GUI related enhancements were made, and known bugs in the underlying UMDES commands were fixed.<br />
<br />
== DESUMA Resources ==<br />
<br />
=== Tutorial ===<br />
:Please visit [[Getting Started with DESUMA2]] for information on using DESUMA2 and its interface.<br />
<br />
:Visit [[DESUMA2 Functions]] for information on the UMDES menu within DESUMA2.<br />
<br />
=== DESUMA Software Download ===<br />
:Click this [https://www.eecs.umich.edu/umdes/projects/lib/download_access/submit_desuma.html link] to download the latest and/or older versions of DESUMA<br />
<br />
:Visit [[DESUMA Installation Instructions]] for proper step by step procedures of installation.<br />
<br />
<br />
== UMDES ==<br />
<br />
UMDES is a library of routines, written in C, for creating and manipulating discrete event systems modeled as FSA. In particular, many of the algorithms for the theory of supervisory control and from the theory of diagnosability of DES are implemented in UMDES. While the main commands in UMDES are embedded within DESUMA, users are still able to run these commands from the command line. For this reason, compiled UMDES commands are available for download.<br />
<br />
'''Note:''' A slight source of confusion is that the names of the UMDES executables do not always exactly match the names of the same commands in DESUMA and DESUMA2 menus for UMDES.<br />
<br />
<br />
=== UMDES Resource ===<br />
<br />
Please go to the [[UMDES Software Library]] page for more information on downloading and using UMDES separately from DESUMA and DESUMA2.<br />
<br />
<br />
== UMDES21 ==<br />
<br />
UMDES21 is a library of routines, written in java, for verifying the opacity of discrete event systems modeled as FSA. In particular, current-state opacity, initial-state opacity, infinite-step opacity, and K-step opacity verification are implemented in UMDES21. The main commands in UMDES21 are embedded within DESUMA, and users are able to run these commands under the UMDES21 menu in DESUMA.<br />
<br />
=== Input Reference ===<br />
<br />
'''Current State Opacity Verifier'''<br />
<br />
:Input: <br />
:1) A graph to perform current-state opacity test on<br />
<br />
::Format: .fsm<br />
<br />
:2) A state data file: a file that lists the names of all the secret states<br />
<br />
::Format: .states<br />
<br />
:Output: <br />
:1) "This fsm obeys current-state opacity"<br />
<br />
:2) "This fsm violates current-state opacity"<br />
<br />
::"The violating states (in the observer) are…”<br />
<br />
<br />
<br />
<br />
'''Initial State Opacity Verifier'''<br />
<br />
:Input:<br />
<br />
:1) A graph to perform initial-state opacity test on<br />
<br />
::Format: .fsm<br />
<br />
:2) An initial state data file: a file that lists the names of all the initial states, and their secrecy status<br />
<br />
::Format: .init<br />
<br />
:Output:<br />
<br />
:1) "This fsm obeys initial-state opacity"<br />
<br />
:2) "This fsm violates initial-state opacity", <br />
<br />
::"The violating states (in the observer of the reversed automaton) are…”<br />
<br />
<br />
<br />
'''Infinite/K-Step Opacity Verifier'''<br />
<br />
:Input: <br />
:1) A graph to perform infinite/K-step opacity test on<br />
<br />
::Format: .fsm<br />
<br />
:2) A state data file: a file that lists the names of all the secret states<br />
<br />
::Format: .states<br />
<br />
:3) K value: infinite step(any input K<0), K-step(the specific value K>=0)<br />
<br />
::Format: integer<br />
<br />
:4) Ultra fast mode: no Two-Way Observer generated; or<br />
<br />
::Fast mode: Two-Way Observer generated<br />
<br />
:Output:<br />
<br />
:1) "This fsm obeys infinite/K step opacity"<br />
<br />
:2) "This fsm violates infinite/K step opacity", <br />
<br />
::"The violating states (in the Two-Way Observer) are…”<br />
<br />
:3) If “Fast Mode” is chosen, the Two-Way Observer will be generated in .fsm format under the directory /temp.<br />
<br />
=== Format Reference ===<br />
1) '''.fsm'''<br />
<br />
:Line1: <#of states><br />
<br />
:Line2: <state name> <marked? 1(Y):0(N)> <#of transitions><br />
<br />
:Line3: <event name> <next state name> <observable? o(Y):uo(N)><br />
<br />
:…<br />
<br />
'''Example:'''<br />
<br />
:4<br />
<br />
:state0 0 2<br />
<br />
:uo state1 uo<br />
<br />
:uo state2 uo<br />
<br />
<br />
:state1 0 2<br />
<br />
:a state3 o<br />
<br />
<br />
:state2 0 1<br />
<br />
:b state1 o<br />
<br />
<br />
:state3 1 1<br />
<br />
:a state2 o<br />
<br />
<br />
<br />
2) '''.states'''<br />
<br />
:Line1: <secret state name1><br />
<br />
:Line2: <secret state name2><br />
<br />
:…<br />
<br />
<br />
'''Example:'''<br />
<br />
:state4<br />
<br />
:state2<br />
<br />
<br />
<br />
3) '''.init'''<br />
<br />
:Line1: <initial state name1> <secret? 1(Y):0(N)><br />
<br />
:Line2: <initial state name2> <secret? 1(Y):0(N)><br />
<br />
:…<br />
<br />
<br />
'''Example:'''<br />
<br />
:state2 1<br />
<br />
:state3 0<br />
<br />
:state0 1</div>Yuweibaohttps://wiki.eecs.umich.edu/desuma/index.php/DESUMADESUMA2017-08-15T17:55:51Z<p>Yuweibao: </p>
<hr />
<div>== DESUMA Software ==<br />
[[File:DESUMA1.png|400px|thumb|right|DESUMA 1.5.4 interface for Windows]]<br />
The Discrete Event System, University of Michigan and Mount Allison University, or DESUMA, is a software and educational tool used to build, analyze and control models of Discrete Event Systems (DES) as finite-state automata (FSA). It consists of the integration between the UMDES library (a set of commands for DES operations), developed at the University of Michigan under [http://web.eecs.umich.edu/~stephane/ Prof. Stephane Lafortune], and the graphical environment for visualizing discrete event systems, called GIDDES (Graphical Interface for the Design of Discrete Event Systems), developed at Mount Allison University under [http://www.mta.ca/~lricker/ Prof. Laurie Ricker]. DESUMA allows the user to perform a variety of manipulations of discrete event systems modeled by FSA related to model-building, fault diagnosis, verification, control under full and partial observation, and decentralized control.<br />
<br />
Continuous development of DESUMA is a joint effort between Mount Allison University (Prof. Ricker and her colleagues) and University of Michigan (Prof. Lafortune and his colleagues).<br />
<br />
'''Note:''' UMDES commands are embedded within the DESUMA software. However, running commands from the command line is also possible. See UMDES section for more.<br />
<br />
<br />
== DESUMA2 ==<br />
[[File:DESUMA2.png|400px|thumb|right|DESUMA 2.0.0 interface for Windows]]<br />
DESUMA2 is the latest software version made public in 2014. Notable changes from the previous DESUMA version include the FSA layout being done using J-Graph instead of GraphViz due to compatibility problems with the latest JAVA versions. Several GUI related enhancements were made, and known bugs in the underlying UMDES commands were fixed.<br />
<br />
== DESUMA Resources ==<br />
<br />
=== Tutorial ===<br />
:Please visit [[Getting Started with DESUMA2]] for information on using DESUMA2 and its interface.<br />
<br />
:Visit [[DESUMA2 Functions]] for information on the UMDES menu within DESUMA2.<br />
<br />
=== DESUMA Software Download ===<br />
:Click this [https://www.eecs.umich.edu/umdes/projects/lib/download_access/submit_desuma.html link] to download the latest and/or older versions of DESUMA<br />
<br />
:Visit [[DESUMA Installation Instructions]] for proper step by step procedures of installation.<br />
<br />
<br />
== UMDES ==<br />
<br />
UMDES is a library of routines, written in C, for creating and manipulating discrete event systems modeled as FSA. In particular, many of the algorithms for the theory of supervisory control and from the theory of diagnosability of DES are implemented in UMDES. While the main commands in UMDES are embedded within DESUMA, users are still able to run these commands from the command line. For this reason, compiled UMDES commands are available for download.<br />
<br />
'''Note:''' A slight source of confusion is that the names of the UMDES executables do not always exactly match the names of the same commands in DESUMA and DESUMA2 menus for UMDES.<br />
<br />
<br />
=== UMDES Resource ===<br />
<br />
Please go to the [[UMDES Software Library]] page for more information on downloading and using UMDES separately from DESUMA and DESUMA2.<br />
<br />
<br />
== UMDES21 ==<br />
<br />
UMDES21 is a library of routines, written in java, for verifying the opacity of discrete event systems modeled as FSA. In particular, current-state opacity, initial-state opacity, infinite-step opacity, and K-step opacity verification are implemented in UMDES21. The main commands in UMDES21 are embedded within DESUMA, and users are able to run these commands under the UMDES21 menu in DESUMA.<br />
<br />
=== Input Reference ===<br />
<br />
'''Current State Opacity Verifier'''<br />
<br />
:Input: <br />
:1) A graph to perform current-state opacity test on<br />
<br />
::Format: .fsm<br />
<br />
:2) A state data file: a file that lists the names of all the secret states<br />
<br />
::Format: .states<br />
<br />
<br />
<br />
'''Initial State Opacity Verifier'''<br />
<br />
:Input:<br />
<br />
:1) A graph to perform initial-state opacity test on<br />
<br />
::Format: .fsm<br />
<br />
:2) An initial state data file: a file that lists the names of all the initial states, and their secrecy status<br />
<br />
::Format: .init<br />
<br />
<br />
<br />
'''Infinite/K-Step Opacity Verifier'''<br />
<br />
:Input: <br />
:1) A graph to perform infinite/K-step opacity test on<br />
<br />
::Format: .fsm<br />
<br />
:2) A state data file: a file that lists the names of all the secret states<br />
<br />
::Format: .states<br />
<br />
:3) K value: infinite step(any input K<0), K-step(the specific value K>=0)<br />
<br />
::Format: integer<br />
<br />
<br />
<br />
=== Format Reference ===<br />
1) '''.fsm'''<br />
<br />
:Line1: <#of states><br />
<br />
:Line2: <state name> <marked? 1(Y):0(N)> <#of transitions><br />
<br />
:Line3: <event name> <next state name> <observable? o(Y):uo(N)><br />
<br />
:…<br />
<br />
'''Example:'''<br />
<br />
:4<br />
<br />
:state0 0 2<br />
<br />
:uo state1 uo<br />
<br />
:uo state2 uo<br />
<br />
<br />
:state1 0 2<br />
<br />
:a state3 o<br />
<br />
<br />
:state2 0 1<br />
<br />
:b state1 o<br />
<br />
<br />
:state3 1 1<br />
<br />
:a state2 o<br />
<br />
<br />
<br />
2) '''.states'''<br />
<br />
:Line1: <secret state name1><br />
<br />
:Line2: <secret state name2><br />
<br />
:…<br />
<br />
<br />
'''Example:'''<br />
<br />
:state4<br />
<br />
:state2<br />
<br />
<br />
<br />
3) '''.init'''<br />
<br />
:Line1: <initial state name1> <secret? 1(Y):0(N)><br />
<br />
:Line2: <initial state name2> <secret? 1(Y):0(N)><br />
<br />
:…<br />
<br />
<br />
'''Example:'''<br />
<br />
:state2 1<br />
<br />
:state3 0<br />
<br />
:state0 1</div>Yuweibaohttps://wiki.eecs.umich.edu/desuma/index.php/DESUMADESUMA2017-08-15T17:48:48Z<p>Yuweibao: /* Format Reference */</p>
<hr />
<div>== DESUMA Software ==<br />
[[File:DESUMA1.png|400px|thumb|right|DESUMA 1.5.4 interface for Windows]]<br />
The Discrete Event System, University of Michigan and Mount Allison University, or DESUMA, is a software and educational tool used to build, analyze and control models of Discrete Event Systems (DES) as finite-state automata (FSA). It consists of the integration between the UMDES library (a set of commands for DES operations), developed at the University of Michigan under [http://web.eecs.umich.edu/~stephane/ Prof. Stephane Lafortune], and the graphical environment for visualizing discrete event systems, called GIDDES (Graphical Interface for the Design of Discrete Event Systems), developed at Mount Allison University under [http://www.mta.ca/~lricker/ Prof. Laurie Ricker]. DESUMA allows the user to perform a variety of manipulations of discrete event systems modeled by FSA related to model-building, fault diagnosis, verification, control under full and partial observation, and decentralized control.<br />
<br />
Continuous development of DESUMA is a joint effort between Mount Allison University (Prof. Ricker and her colleagues) and University of Michigan (Prof. Lafortune and his colleagues).<br />
<br />
'''Note:''' UMDES commands are embedded within the DESUMA software. However, running commands from the command line is also possible. See UMDES section for more.<br />
<br />
<br />
== DESUMA2 ==<br />
[[File:DESUMA2.png|400px|thumb|right|DESUMA 2.0.0 interface for Windows]]<br />
DESUMA2 is the latest software version made public in 2014. Notable changes from the previous DESUMA version include the FSA layout being done using J-Graph instead of GraphViz due to compatibility problems with the latest JAVA versions. Several GUI related enhancements were made, and known bugs in the underlying UMDES commands were fixed.<br />
<br />
== DESUMA Resources ==<br />
<br />
=== Tutorial ===<br />
:Please visit [[Getting Started with DESUMA2]] for information on using DESUMA2 and its interface.<br />
<br />
:Visit [[DESUMA2 Functions]] for information on the UMDES menu within DESUMA2.<br />
<br />
=== DESUMA Software Download ===<br />
:Click this [https://www.eecs.umich.edu/umdes/projects/lib/download_access/submit_desuma.html link] to download the latest and/or older versions of DESUMA<br />
<br />
:Visit [[DESUMA Installation Instructions]] for proper step by step procedures of installation.<br />
<br />
<br />
== UMDES ==<br />
<br />
UMDES is a library of routines, written in C, for creating and manipulating discrete event systems modeled as FSA. In particular, many of the algorithms for the theory of supervisory control and from the theory of diagnosability of DES are implemented in UMDES. While the main commands in UMDES are embedded within DESUMA, users are still able to run these commands from the command line. For this reason, compiled UMDES commands are available for download.<br />
<br />
'''Note:''' A slight source of confusion is that the names of the UMDES executables do not always exactly match the names of the same commands in DESUMA and DESUMA2 menus for UMDES.<br />
<br />
<br />
=== UMDES Resource ===<br />
<br />
Please go to the [[UMDES Software Library]] page for more information on downloading and using UMDES separately from DESUMA and DESUMA2.<br />
<br />
<br />
== UMDES21 ==<br />
<br />
UMDES21 is a library of routines, written in java, for verifying the opacity of discrete event systems modeled as FSA. In particular, current-state opacity, initial-state opacity, infinite-step opacity, and K-step opacity verification are implemented in UMDES21. The main commands in UMDES21 are embedded within DESUMA, and users are able to run these commands under the UMDES21 menu in DESUMA.<br />
<br />
=== Input Reference ===<br />
<br />
'''Current State Opacity Verifier'''<br />
<br />
Input: <br />
1) A graph to perform current-state opacity test on<br />
<br />
Format: .fsm<br />
<br />
2) A state data file: a file that lists the names of all the secret states<br />
<br />
Format: .states<br />
<br />
<br />
<br />
'''Initial State Opacity Verifier'''<br />
<br />
Input:<br />
<br />
1) A graph to perform initial-state opacity test on<br />
<br />
Format: .fsm<br />
<br />
2) An initial state data file: a file that lists the names of all the initial states, and their secrecy status<br />
<br />
Format: .init<br />
<br />
<br />
<br />
'''Infinite/K-Step Opacity Verifier'''<br />
<br />
Input: <br />
1) A graph to perform infinite/K-step opacity test on<br />
<br />
Format: .fsm<br />
<br />
2) A state data file: a file that lists the names of all the secret states<br />
<br />
Format: .states<br />
<br />
3) K value: infinite step(any input K<0), K-step(the specific value K>=0)<br />
<br />
Format: integer<br />
<br />
<br />
<br />
=== Format Reference ===<br />
1) '''.fsm'''<br />
<br />
Line1: <#of states><br />
<br />
Line2: <state name> <marked? 1(Y):0(N)> <#of transitions><br />
<br />
Line3: <event name> <next state name> <observable? o(Y):uo(N)><br />
<br />
…<br />
<br />
'''Example:'''<br />
<br />
4<br />
<br />
state0 0 2<br />
<br />
uo state1 uo<br />
<br />
uo state2 uo<br />
<br />
<br />
state1 0 2<br />
<br />
a state3 o<br />
<br />
<br />
state2 0 1<br />
<br />
b state1 o<br />
<br />
<br />
state3 1 1<br />
<br />
a state2 o<br />
<br />
<br />
<br />
2) '''.states'''<br />
<br />
Line1: <secret state name1><br />
<br />
Line2: <secret state name2><br />
<br />
…<br />
<br />
<br />
'''Example:'''<br />
<br />
state4<br />
<br />
state2<br />
<br />
<br />
<br />
3) '''.init'''<br />
<br />
Line1: <initial state name1> <secret? 1(Y):0(N)><br />
<br />
Line2: <initial state name2> <secret? 1(Y):0(N)><br />
<br />
…<br />
<br />
<br />
'''Example:'''<br />
<br />
state2 1<br />
<br />
state3 0<br />
<br />
state0 1</div>Yuweibaohttps://wiki.eecs.umich.edu/desuma/index.php/DESUMADESUMA2017-08-15T17:47:51Z<p>Yuweibao: Add UMDES21</p>
<hr />
<div>== DESUMA Software ==<br />
[[File:DESUMA1.png|400px|thumb|right|DESUMA 1.5.4 interface for Windows]]<br />
The Discrete Event System, University of Michigan and Mount Allison University, or DESUMA, is a software and educational tool used to build, analyze and control models of Discrete Event Systems (DES) as finite-state automata (FSA). It consists of the integration between the UMDES library (a set of commands for DES operations), developed at the University of Michigan under [http://web.eecs.umich.edu/~stephane/ Prof. Stephane Lafortune], and the graphical environment for visualizing discrete event systems, called GIDDES (Graphical Interface for the Design of Discrete Event Systems), developed at Mount Allison University under [http://www.mta.ca/~lricker/ Prof. Laurie Ricker]. DESUMA allows the user to perform a variety of manipulations of discrete event systems modeled by FSA related to model-building, fault diagnosis, verification, control under full and partial observation, and decentralized control.<br />
<br />
Continuous development of DESUMA is a joint effort between Mount Allison University (Prof. Ricker and her colleagues) and University of Michigan (Prof. Lafortune and his colleagues).<br />
<br />
'''Note:''' UMDES commands are embedded within the DESUMA software. However, running commands from the command line is also possible. See UMDES section for more.<br />
<br />
<br />
== DESUMA2 ==<br />
[[File:DESUMA2.png|400px|thumb|right|DESUMA 2.0.0 interface for Windows]]<br />
DESUMA2 is the latest software version made public in 2014. Notable changes from the previous DESUMA version include the FSA layout being done using J-Graph instead of GraphViz due to compatibility problems with the latest JAVA versions. Several GUI related enhancements were made, and known bugs in the underlying UMDES commands were fixed.<br />
<br />
== DESUMA Resources ==<br />
<br />
=== Tutorial ===<br />
:Please visit [[Getting Started with DESUMA2]] for information on using DESUMA2 and its interface.<br />
<br />
:Visit [[DESUMA2 Functions]] for information on the UMDES menu within DESUMA2.<br />
<br />
=== DESUMA Software Download ===<br />
:Click this [https://www.eecs.umich.edu/umdes/projects/lib/download_access/submit_desuma.html link] to download the latest and/or older versions of DESUMA<br />
<br />
:Visit [[DESUMA Installation Instructions]] for proper step by step procedures of installation.<br />
<br />
<br />
== UMDES ==<br />
<br />
UMDES is a library of routines, written in C, for creating and manipulating discrete event systems modeled as FSA. In particular, many of the algorithms for the theory of supervisory control and from the theory of diagnosability of DES are implemented in UMDES. While the main commands in UMDES are embedded within DESUMA, users are still able to run these commands from the command line. For this reason, compiled UMDES commands are available for download.<br />
<br />
'''Note:''' A slight source of confusion is that the names of the UMDES executables do not always exactly match the names of the same commands in DESUMA and DESUMA2 menus for UMDES.<br />
<br />
<br />
=== UMDES Resource ===<br />
<br />
Please go to the [[UMDES Software Library]] page for more information on downloading and using UMDES separately from DESUMA and DESUMA2.<br />
<br />
<br />
== UMDES21 ==<br />
<br />
UMDES21 is a library of routines, written in java, for verifying the opacity of discrete event systems modeled as FSA. In particular, current-state opacity, initial-state opacity, infinite-step opacity, and K-step opacity verification are implemented in UMDES21. The main commands in UMDES21 are embedded within DESUMA, and users are able to run these commands under the UMDES21 menu in DESUMA.<br />
<br />
=== Input Reference ===<br />
<br />
'''Current State Opacity Verifier'''<br />
<br />
Input: <br />
1) A graph to perform current-state opacity test on<br />
<br />
Format: .fsm<br />
<br />
2) A state data file: a file that lists the names of all the secret states<br />
<br />
Format: .states<br />
<br />
<br />
<br />
'''Initial State Opacity Verifier'''<br />
<br />
Input:<br />
<br />
1) A graph to perform initial-state opacity test on<br />
<br />
Format: .fsm<br />
<br />
2) An initial state data file: a file that lists the names of all the initial states, and their secrecy status<br />
<br />
Format: .init<br />
<br />
<br />
<br />
'''Infinite/K-Step Opacity Verifier'''<br />
<br />
Input: <br />
1) A graph to perform infinite/K-step opacity test on<br />
<br />
Format: .fsm<br />
<br />
2) A state data file: a file that lists the names of all the secret states<br />
<br />
Format: .states<br />
<br />
3) K value: infinite step(any input K<0), K-step(the specific value K>=0)<br />
<br />
Format: integer<br />
<br />
<br />
<br />
=== Format Reference ===<br />
1) '''.fsm'''<br />
<br />
Line1: <#of states><br />
<br />
Line2: <state name> <marked? 1(Y):0(N)> <#of transitions><br />
<br />
Line3: <event name> <next state name> <observable? o(Y):uo(N)><br />
<br />
…<br />
<br />
'''Example:'''<br />
4<br />
<br />
state0 0 2<br />
<br />
uo state1 uo<br />
<br />
uo state2 uo<br />
<br />
<br />
state1 0 2<br />
<br />
a state3 o<br />
<br />
<br />
state2 0 1<br />
<br />
b state1 o<br />
<br />
<br />
state3 1 1<br />
<br />
a state2 o<br />
<br />
<br />
<br />
2) '''.states'''<br />
<br />
Line1: <secret state name1><br />
<br />
Line2: <secret state name2><br />
<br />
…<br />
<br />
<br />
'''Example:'''<br />
<br />
state4<br />
<br />
state2<br />
<br />
<br />
<br />
3) '''.init'''<br />
<br />
Line1: <initial state name1> <secret? 1(Y):0(N)><br />
<br />
Line2: <initial state name2> <secret? 1(Y):0(N)><br />
<br />
…<br />
<br />
<br />
'''Example:'''<br />
<br />
state2 1<br />
<br />
state3 0<br />
<br />
state0 1</div>Yuweibao