# UMDES Commands

(→Control) |
|||

Line 82: | Line 82: | ||

[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. | [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. | ||

− | 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/Infcon 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). | + | [https://wiki.eecs.umich.edu/desuma/index.php/Normal 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). | + | [https://wiki.eecs.umich.edu/desuma/index.php/Obs 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). | + | [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_pc: Builds the supremal controllable normal sublanguage of L(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). |

− | supcon1: Builds the supremal controllable sublanguage of L_m(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). |

− | supcon_std. Builds the supremal controllable sublanguage of L(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). |

− | supnorm: Builds the supremal controllable sublanguage of L_m(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). |

− | 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. | + | [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. |

== Failure Diagnosis == | == Failure Diagnosis == | ||

− | compose: Generates the composite system with the appropriate sensor readings for each state | + | [https://wiki.eecs.umich.edu/desuma/index.php/Compose 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. | |

− | + | [https://wiki.eecs.umich.edu/desuma/index.php/Diag_a 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. | |

− | + | [https://wiki.eecs.umich.edu/desuma/index.php/Diag_UR 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. | |

− | + | [https://wiki.eecs.umich.edu/desuma/index.php/Idiag 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. | |

− | + | [https://wiki.eecs.umich.edu/desuma/index.php/Dcycle 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. | |

− | + | [https://wiki.eecs.umich.edu/desuma/index.php/R_diag 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. | |

− | verifier_decen_dia: Builds verifiers to test diagnosibility in a decentralized system. | + | [https://wiki.eecs.umich.edu/desuma/index.php/Verifier_dia 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. | ||

== Stochastic Diagnosability == | == Stochastic Diagnosability == |

## Revision as of 17:57, 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.