UMDES Commands

From DESUMA Wiki
UMDES Commands
Jump to: navigation, search

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