Commands : Input/Output
Routines | Manipulation of FSM | Control
| Failure Diagnosis | Stochastic
Diagnosis
File Formats : Format of Input Files | Format of Output Files
KEY | |
Click for detailed information and examples. | |
Command accepts NDFAs with EMPTY_TRACE transitions. | |
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 | |
acc | Removes incaccessible states from the FSM. |
change_cprop | Changes controllability properties of events. |
change_initial_state | Change the inital state of the FSM. |
change_oprop | Changes observability properties of events. |
c_par_comp | Creates the constrained parallel composition of the set of FSM's. |
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. |
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 L_{m}(H) contains L_{m}(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. |
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. |
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 the observer of the FSM in diagnoser or FSM format. |
par_comp | Creates the parallel composition of the set of FSM's. |
product | Creates the product of the two FSM's. |
refine | Refines a system model subject to a given specification 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. |
trim | Returns the accessible and co-accessible part of an FSM. |
union | Creates a machine whose language is the union of the two FSM's. |
Control | |
coobs | Tests for the coobserability of L(H) with respect to L(G), with two agents. |
coobs_gen | General form 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 disabled 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 sub--language of the intersection of L_{m}(G) and L_{m}(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 diagnosibility 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-diagnosibility of the FSM by detecing (Fi,Ii)-indeterminate cycles. |
dcycle | Tests for diagnosibility 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 diagnosability. |
verifier_decen_dia | Builds verifiers to test diagnosability 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. |
Last updated: July 29, 2005 |
KEY | |
Format of Input Files | |
machine.fsm | Data for individual FSM |
machine.stoc | Stochastic data for machine.fsm |
glob_sens.map | Global sensor map for sensmap |
sensor_data.map | Sensor data map for the system |
events.ift | Events map for the system (I-diagnosibility) |
g.ft | Failure partition for building diagnoser |
Format of Output Files | |
g.fsm | Data for individual FSM (same as input FSM) |
g.diag | Diagnoser of FSM. |
h_diag.fsm | Diagnoser written in FSM format |
g.idiag | I-Diagnoser of FSM |
g.sdiag | Diagnoser of FSM in simplifed format |
h.cycles | Fi-indeterminate cycles in h.diag |
hi.cycles | (Fi,Ii)-indeterminate cycles in hi.diag |
Last updated: July 29, 2005 |
UMDES-LIB Contact Information: Please e-mail questions to: desuma-help AT eecs DOT umich DOT edu. Although we are unable to provide full technical support, we will do our best to help.