Commands : Input/Output Routines | Manipulation of FSM | Control | Failure Diagnosis | Stochastic Diagnosis

File Formats : Format of Input Files | Format of Output Files

Commands

KEY
	Click for detailed information and examples.
	Command accepts NDFAs with EMPTY_TRACE transitions.
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
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 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.
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 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 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

File Formats

up to Top

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.