UMDES-LIB Software Library


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

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



icon.jpg (5406 bytes)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


icon.jpg (5406 bytes)File Formats

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

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.