UMDES Commands

From DESUMA Wiki
UMDES Commands
Jump to: navigation, search
Line 27: Line 27:
 
[[change_cprop]]: Changes controllability properties of events.
 
[[change_cprop]]: Changes controllability properties of events.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Change_initial_state change_initial_state]: Change the initial state of the FSM.
+
[[change_initial_state]]: Change the initial state of the FSM.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Change_oprop change_oprop]: Changes observability properties of events.
+
[[change_oprop]]: Changes observability properties of events.
  
[https://wiki.eecs.umich.edu/desuma/index.php/C_par_comp c_par_comp]: Creates the constrained parallel composition of the set of FSMs.
+
[[c_par_comp]]: Creates the constrained parallel composition of the set of FSMs.
  
[X][O] [https://wiki.eecs.umich.edu/desuma/index.php/Co_acc co_acc]: Obtains the co-accessible part of the FSM.
+
[X][O] [[co_acc]]: Obtains the co-accessible part of the FSM.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Comp_fsm comp_fsm]: Returns the complement of the FSM.
+
[[comp_fsm]]: Returns the complement of the FSM.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Concat concat]: Returns the concatenation of the two input FSM's.
+
[[concat]]: Returns the concatenation of the two input FSM's.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Concat_ev concat_ev]: Adds transitions to the DEAD state for all events in the event list.
+
[[concat_ev]]: Adds transitions to the DEAD state for all events in the event list.
  
[O] [https://wiki.eecs.umich.edu/desuma/index.php/Conflict conflict]: Tests for non-conflicting languages of the two FSM's.
+
[O] [[conflict]]: Tests for non-conflicting languages of the two FSM's.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Equiv equiv]: Tests for the language equivalence of two FSM's.
+
[[equiv]]: Tests for the language equivalence of two FSM's.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Incl incl]: Tests if L(H) contains L(G) and if Lm(H) contains Lm(G) where H and G are two input FSMs.
+
[[incl]]: Tests if L(H) contains L(G) and if Lm(H) contains Lm(G) where H and G are two input FSMs.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Inv_p_L inv_p_L]: Returns the inverse projection of the FSM with respect to another one and the given event list.
+
[[inv_p_L]]: Returns the inverse projection of the FSM with respect to another one and the given event list.
  
[X] [https://wiki.eecs.umich.edu/desuma/index.php/Inv_proj inv_proj]: Returns the inverse projection of the FSM with respect to the given event list.
+
[X] [[inv_proj]]: Returns the inverse projection of the FSM with respect to the given event list.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Live live]: Returns a live FSM given a non-live one by adding self-loops to all DEAD states.
+
[[live]]: Returns a live FSM given a non-live one by adding self-loops to all DEAD states.
  
[X] [https://wiki.eecs.umich.edu/desuma/index.php/Mark_fsm mark_fsm]: Marks all the states in the FSM.
+
[X] [[mark_fsm]]: Marks all the states in the FSM.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Minimize_std minimize_std]: Checks for and removes equivalent states from the FSM using the standard algorithm.
+
[[minimize_std]]: Checks for and removes equivalent states from the FSM using the standard algorithm.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Obsvr obsvr]: Returns observer of the FSM in diagnoser or FSM format.
+
[[obsvr]]: Returns observer of the FSM in diagnoser or FSM format.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Par_comp par_comp]: Creates the parallel composition of the set of FMS's.
+
[[par_comp]]: Creates the parallel composition of the set of FMS's.
  
[X] [https://wiki.eecs.umich.edu/desuma/index.php/Product product]: Creates the product of two FSM's.
+
[X] [[product]]: Creates the product of two FSM's.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Refine refine]: Refines a system model subject to a given speculation model.
+
[[refine]]: Refines a system model subject to a given speculation model.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Rename_dead rename_dead]: Renames the DEAD state of an FSM to DEADi.
+
[[rename_dead]]: Renames the DEAD state of an FSM to DEADi.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Rename_states rename_states]: Renames the states in the FSM, counting up from 1.
+
[[rename_states]]: Renames the states in the FSM, counting up from 1.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Rm_state rm_state]: Removes the listed states from the FSM.
+
[[rm_state]]: Removes the listed states from the FSM.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Union union]: Creates a machine whose language is the union of two FSM's.
+
[[union]]: Creates a machine whose language is the union of two FSM's.
  
 
== Control ==
 
== Control ==
  
[https://wiki.eecs.umich.edu/desuma/index.php/Coobs coobs]: Tests for the coobservability of L(H) with respect to L(G), with two agents.
+
[[coobs]]: Tests for the coobservability of L(H) with respect to L(G), with two agents.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Coobs_gen coobs_gen]: General forms of coobs dealing with multiple site and generalized coobservability.
+
[[coobs_gen]]: General forms of coobs dealing with multiple site and generalized coobservability.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Ctrb ctrb]: Tests for the controllability of L_m(H) with respect to L(G) and a set of uncontrollable events.
+
[[ctrb]]: Tests for the controllability of L_m(H) with respect to L(G) and a set of uncontrollable events.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Enable_map enable_map]: Lists events that are enabled or disables at each state of a supervisor FSM with respect to a system FSM.
+
[[enable_map]]: Lists events that are enabled or disables at each state of a supervisor FSM with respect to a system FSM.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Infcon infcon]: Generates the infimal prefix-closed and controllable super-language of a given language with respect to a second prefix-closed language.
+
[[infcon]]: Generates the infimal prefix-closed and controllable super-language of a given language with respect to a second prefix-closed language.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Normal normal]: Tests for the normality of L(H) with respect to L(G).
+
[[normal]]: Tests for the normality of L(H) with respect to L(G).
  
[https://wiki.eecs.umich.edu/desuma/index.php/Obs obs]: Tests for the observability of L(H) with respect to L(G).
+
[[obs]]: Tests for the observability of L(H) with respect to L(G).
  
[https://wiki.eecs.umich.edu/desuma/index.php/Supcn supcn]: Builds the supremal controllable normal sublanguage of L_m(H) with respect to L(G).
+
[[supcn]]: Builds the supremal controllable normal sublanguage of L_m(H) with respect to L(G).
  
[https://wiki.eecs.umich.edu/desuma/index.php/Supcn_pc supcn_pc]: Builds the supremal controllable normal sublanguage of L(H) with respect to L(G).
+
[[supcn_pc]]: Builds the supremal controllable normal sublanguage of L(H) with respect to L(G).
  
[https://wiki.eecs.umich.edu/desuma/index.php/Supcon1 supcon1]: Builds the supremal controllable sublanguage of L_m(H) with respect to L(G).
+
[[supcon1]]: Builds the supremal controllable sublanguage of L_m(H) with respect to L(G).
  
[https://wiki.eecs.umich.edu/desuma/index.php/Supcon_std supcon_std]. Builds the supremal controllable sublanguage of L(H) with respect to L(G).
+
[[supcon_std]]. Builds the supremal controllable sublanguage of L(H) with respect to L(G).
  
[https://wiki.eecs.umich.edu/desuma/index.php/Supnorm supnorm]: Builds the supremal controllable sublanguage of L_m(H) with respect to L(G).
+
[[supnorm]]: Builds the supremal controllable sublanguage of L_m(H) with respect to L(G).
  
[https://wiki.eecs.umich.edu/desuma/index.php/Vlp_s vlp_s]: Builds an FSM, H_sup.fsm, whose marked language is the supremal controllable sublanguage of the intersection of Lm(G) and Lm(H) with respect to L(G) and E{uc}, the uncontrollable event set of G.
+
[[vlp_s]]: Builds an FSM, H_sup.fsm, whose marked language is the supremal controllable sublanguage of the intersection of Lm(G) and Lm(H) with respect to L(G) and E{uc}, the uncontrollable event set of G.
  
 
== Failure Diagnosis ==
 
== Failure Diagnosis ==
  
[https://wiki.eecs.umich.edu/desuma/index.php/Compose compose]: Generates the composite system with the appropriate sensor readings for each state.
+
[[compose]]: Generates the composite system with the appropriate sensor readings for each state.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Diag diag]: Generates the (multiple fault) diagnoser for the given FSM.
+
[[diag]]: Generates the (multiple fault) diagnoser for the given FSM.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Diag_a diag_a]: Generates the diagnoser (with ambiguous labels) for the FSM.
+
[[diag_a]]: Generates the diagnoser (with ambiguous labels) for the FSM.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Diag_EX diag_EX]: Generates the extended diagnoser for the FSM.
+
[[diag_EX]]: Generates the extended diagnoser for the FSM.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Diag_UR diag_UR]: Generates the diagnoser with unobservable reach.
+
[[diag_UR]]: Generates the diagnoser with unobservable reach.
  
[https://wiki.eecs.umich.edu/desuma/index.php/R_cycle r_cycle]: Tests for diagnosability of an intermittent-fault FSM by looking for type o, type i, type p and type r indeterminate cycles.
+
[[r_cycle]]: Tests for diagnosability of an intermittent-fault FSM by looking for type o, type i, type p and type r indeterminate cycles.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Idiag idiag]: Generates the I-diagnoser of the FSM.
+
[[idiag]]: Generates the I-diagnoser of the FSM.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Dicycle dicycle]: Tests for I-diagnosability of the FSM by detecting (Fi,li)-indeterminate cycles.
+
[[dicycle]]: Tests for I-diagnosability of the FSM by detecting (Fi,li)-indeterminate cycles.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Dcycle dcycle]: Tests for diagnosability of the FSM by detecting Fi-indeterminate cycles.
+
[[dcycle]]: Tests for diagnosability of the FSM by detecting Fi-indeterminate cycles.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Eventmap eventmap]: Maps the indicator events to the observable states in the FSM.
+
[[eventmap]]: Maps the indicator events to the observable states in the FSM.
  
[https://wiki.eecs.umich.edu/desuma/index.php/R_diag r_diag]: Builds a diagnoser that can handle reset events.
+
[[r_diag]]: Builds a diagnoser that can handle reset events.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Sensmap sensmap]: Maps the sensor readings to every state in the FSM.
+
[[sensmap]]: Maps the sensor readings to every state in the FSM.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Verifier_dia verifier_dia]: Builds verifiers to test diagnosibility.
+
[[verifier_dia]]: Builds verifiers to test diagnosibility.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Verifier_decen_dia verifier_decen_dia]: Builds verifiers to test diagnosibility in a decentralized system.
+
[[verifier_decen_dia]]: Builds verifiers to test diagnosibility in a decentralized system.
  
 
== Stochastic Diagnosability ==
 
== Stochastic Diagnosability ==
  
[https://wiki.eecs.umich.edu/desuma/index.php/A_diagnosability a_diagnosability]: Tests for A-Diagnosability by looking at the given FSM's stochastic diagnoser.
+
[[a_diagnosability]]: Tests for A-Diagnosability by looking at the given FSM's stochastic diagnoser.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Create_sfsm create_sfsm]: Interactive routine to create stochastic information files for an existing FSM.
+
[[create_sfsm]]: Interactive routine to create stochastic information files for an existing FSM.
  
[https://wiki.eecs.umich.edu/desuma/index.php/Sdiag sdiag]: Generates the stochastic diagnoser for the given FSM.
+
[[sdiag]]: Generates the stochastic diagnoser for the given FSM.

Revision as of 18:59, July 29, 2013

Commands for UMDES software, when used from the command line, are listed here.

Historical note: UMDES uses the terminology FSM (finite state machine) instead of FSA.

If denoted by [X], the command accepts NDFM (nondeterministic finite state machines) with EMPTY_TRACE transitions.

If denoted by [O], click the command for detailed information and examples. TODO!

Contents

Input/Output Routines

create_fsm: Interactive routine to create FSM file.

forbid: Writes the list of states that have more than threshold number of individual states.

write_ev: Writes all the events in the FSM.

write_o: Writes all the observable events in the FSM.

write_st: Writes all the states in the FSM.

write_uo: Writes all the unobservable events in the FSM.

Manipulation of FSM

[X][O] acc: Removes inaccessible states from the FSM.

change_cprop: Changes controllability properties of events.

change_initial_state: Change the initial state of the FSM.

change_oprop: Changes observability properties of events.

c_par_comp: Creates the constrained parallel composition of the set of FSMs.

[X][O] co_acc: Obtains the co-accessible part of the FSM.

comp_fsm: Returns the complement of the FSM.

concat: Returns the concatenation of the two input FSM's.

concat_ev: Adds transitions to the DEAD state for all events in the event list.

[O] conflict: Tests for non-conflicting languages of the two FSM's.

equiv: Tests for the language equivalence of two FSM's.

incl: Tests if L(H) contains L(G) and if Lm(H) contains Lm(G) where H and G are two input FSMs.

inv_p_L: Returns the inverse projection of the FSM with respect to another one and the given event list.

[X] inv_proj: Returns the inverse projection of the FSM with respect to the given event list.

live: Returns a live FSM given a non-live one by adding self-loops to all DEAD states.

[X] mark_fsm: Marks all the states in the FSM.

minimize_std: Checks for and removes equivalent states from the FSM using the standard algorithm.

obsvr: Returns observer of the FSM in diagnoser or FSM format.

par_comp: Creates the parallel composition of the set of FMS's.

[X] product: Creates the product of two FSM's.

refine: Refines a system model subject to a given speculation model.

rename_dead: Renames the DEAD state of an FSM to DEADi.

rename_states: Renames the states in the FSM, counting up from 1.

rm_state: Removes the listed states from the FSM.

union: Creates a machine whose language is the union of two FSM's.

Control

coobs: Tests for the coobservability of L(H) with respect to L(G), with two agents.

coobs_gen: General forms of coobs dealing with multiple site and generalized coobservability.

ctrb: Tests for the controllability of L_m(H) with respect to L(G) and a set of uncontrollable events.

enable_map: Lists events that are enabled or disables at each state of a supervisor FSM with respect to a system FSM.

infcon: Generates the infimal prefix-closed and controllable super-language of a given language with respect to a second prefix-closed language.

normal: Tests for the normality of L(H) with respect to L(G).

obs: Tests for the observability of L(H) with respect to L(G).

supcn: Builds the supremal controllable normal sublanguage of L_m(H) with respect to L(G).

supcn_pc: Builds the supremal controllable normal sublanguage of L(H) with respect to L(G).

supcon1: Builds the supremal controllable sublanguage of L_m(H) with respect to L(G).

supcon_std. Builds the supremal controllable sublanguage of L(H) with respect to L(G).

supnorm: Builds the supremal controllable sublanguage of L_m(H) with respect to L(G).

vlp_s: Builds an FSM, H_sup.fsm, whose marked language is the supremal controllable sublanguage of the intersection of Lm(G) and Lm(H) with respect to L(G) and E{uc}, the uncontrollable event set of G.

Failure Diagnosis

compose: Generates the composite system with the appropriate sensor readings for each state.

diag: Generates the (multiple fault) diagnoser for the given FSM.

diag_a: Generates the diagnoser (with ambiguous labels) for the FSM.

diag_EX: Generates the extended diagnoser for the FSM.

diag_UR: Generates the diagnoser with unobservable reach.

r_cycle: Tests for diagnosability of an intermittent-fault FSM by looking for type o, type i, type p and type r indeterminate cycles.

idiag: Generates the I-diagnoser of the FSM.

dicycle: Tests for I-diagnosability of the FSM by detecting (Fi,li)-indeterminate cycles.

dcycle: Tests for diagnosability of the FSM by detecting Fi-indeterminate cycles.

eventmap: Maps the indicator events to the observable states in the FSM.

r_diag: Builds a diagnoser that can handle reset events.

sensmap: Maps the sensor readings to every state in the FSM.

verifier_dia: Builds verifiers to test diagnosibility.

verifier_decen_dia: Builds verifiers to test diagnosibility in a decentralized system.

Stochastic Diagnosability

a_diagnosability: Tests for A-Diagnosability by looking at the given FSM's stochastic diagnoser.

create_sfsm: Interactive routine to create stochastic information files for an existing FSM.

sdiag: Generates the stochastic diagnoser for the given FSM.

Personal tools
Namespaces
Variants
Actions
Navigation
Toolbox
EECS @ UM
Tools