UMDES Commands
Commands for UMDES software, when used from the command line, are listed here.
Note: UMDES uses the terminology FSM (finite-state machine) instead of FSA.
Note: If denoted by [★], the command accepts NDFM (nondeterministic finite state machines) with EMPTY_TRACE transitions.
Note: If denoted by [♦], click the command for detailed information and examples.
Input/Output Routines
create_fsm
Interactive routine to create FSM file.
- File: create_fsm
- Description: This program guides the user through creating a Finite-State Machine from scratch.
- Input: Interactive.
- Output: Created FSM
forbid
Writes the list of states that have more than threshold number of individual states.
- File: forbid
- Description: This program inputs a threshold and a set of failure maps (the format for these files is the same as the sensor maps, but order does not matter). The failure maps represent all the states in the composite machines with failures marked with a 'f' an non-failures marked with a 'NF'. The program outputs the list of compsoite states that have more than threshold number of individual failure states. This set of forbidden states can be used as the input for the constrained synchronous composition program (o_par_comp).
- Input:
- Threshold - Failure threshold
- Component1.map - First failure map
- Component2.map - Second failure map
- ...- more maps
- Output: forbidden.states - List of forbidden composite states.
write_ev
Writes all the events in the FSM.
- File: write_ev
- Description: This program writes all the events found in the given FSM into an events data file.
- Input: h.fsm - Input FSM
- Output: h.events - List of events in h.fsm
write_o
Writes all the observable events in the FSM.
- File: write_o
- Description: This program writes all the observable events in the FSM into an events data file.
- Input: h.fsm - Input FSM
- Output: h.events - List of observable events in h.fsm
write_st
Writes all the states in the FSM.
- File: write_st
- Description: This program writes all the states found in the given FSM into a states data file.
- Input: h.fsm - Input FSM
- Output: h.states - List of states in h.fsm
write_uo
Writes all the unobservable events in the FSM.
- File: write_uo
- Description: This program writes all the uncontrollable events in the FSM to the given output file.
- Input: h.fsm - Input FSM
- Output: h.uo - List of uncontrollable events in h.fsm
Manipulation of FSM
acc
[★][♦] Removes inaccessible states from the FSM.
- File: acc
- Description: This program removes inaccessible states from the given FSM h and returns FSM h_acc which contains only the states accessible from the initial state.
- Input: H.fsm - Input FSM
- Output: H_acc.fsm - Accessible FSM
change_cprop
Changes controllability properties of events.
- File: change_cprop
- Description: This program changes the controllability properties of a given FSM. The routine has three modes:
- ADD will add the events to the uncontrollable events list if they are not on it.
- REMOVE will remove the events from the uncontrollable events list if they are on it.
- CHANGE will add the events to the uncontrollable events list and remove all other events from the list.
- When run interactively, the user has an option of either inputting a file containing the events or inputting events manually. If an output file containing the events or inputting events manually. If an output file is specified, the FSM with the updated event properties will be written to that file. If no file is specified, the original input file will be overwritten.
- Input:
- H.fsm - FSM
- mode - a/r/c for the ADD, REMOVE, or CHANGE mode
- input_format - for interactive mode only: 1 to input a file list, 0 to enter manually. h.e - Uncontrollable events list (if input_format is 1)
- Output: output.fsm - FSM with updated properties (written to input FSM file if no output file is specified)
change_initial_state
Change the initial state of the FSM.
- File: change_initial_state
- Description: This program changes the intial state of the FSM to another state already in the FSM
- Input:
- A.fsm - Input FSM
- state_name - Name of state in A.fsm to be initial state
- Output: out.fsm - The input FSM with initial state changed
change_oprop
Changes observability properties of events.
- File: change_oprop
- Description: This program changes the observability properties of a given FSM. The routine has three modes:
- ADD will add the events to the unobservable events list if they are not on it.
- REMOVE will remove the events from the unobservable events list if they are on it.
- CHANGE will add the events to the unobservable events list and remove all other events from the list.
- When run interactively, the user has an option of either inputting a file containing the events or inputting events manually. If an output file containing the events or inputting events manually. If an output file is specified, the FSM with the updated event properties will be written to that file. If no file is specified, the original input file will be overwritten.
- Input:
- H.fsm - FSM
- mode - a/r/c for the ADD, REMOVE, or CHANGE mode
- input_format - for interactive mode only: 1 to input a file list, 0 to enter manually. h.e - Unobservable events list (if input_format is 1)
- Output: output.fsm - FSM with updated properties (written to input FSM file if no output file is specified
c_par_comp
Creates the constrained parallel composition of the set of FSMs.
- File: c_par_comp
- Description: Constrained Synchronous Composition. This is a modification of synchronous composition that removes a prespecified set of forbidden states from the composite FSM.
- Input:
- Number of Machines
- forbid.states - Set of forbidden states
- component1.fsm - Input FSM 1
- .... - more input FSMs
- Output: c_sync.fsm - Cosntrained Synchronous FSM
co_acc
[★][♦]Obtains the co-accessible part of the FSM.
- File: co_acc.c
- Description: This program obtains the co-accessible part of the FSM h. A co-accessible machine is an accessible machine such that any state can reach a marked state.
- Input: H.fsm - Input FSM
- Output: H_co_acc.fsm - Co-accessible FSM
comp_fsm
Returns the complement of the FSM.
- File: comp_fsm
- Description: This program creates and returns the complement of the given FSM, i.e., the language marked by h_comp.fsm is the complement of the language marked by h.fsm with respect to the Kleene closure of the events in h.fsm.
- Input: H.fsm - Input FSM
- Output: H_comp.fsm - Complement FSM
concat
Returns the concatenation of the two input FSM's.
- File: concat
- Description: This program creates a new FSM which is a concatenation of the two input FSMs. Therefore, Lm(gh) = Lm(g)Lm(h).
- Input:
- G.fsm - First FSM
- H.fsm - Second FSM
- Output: GH.fsm - concatenated FSM
concat_ev
Adds transitions to the DEAD state for all events in the event list.
- File: concat_ev
- Description: At every marked state in the given FSM. this program adds a transition to the DEAD state (added) for every event in A.events not in the active event set of the states in g.fsm. It also adds self-loops for A.events at the DEAD state. Thus, Lm(gA) = Lm(g)A*
- Input:
- H.fsm - Input FSM
- A.events - List of events to be concatenated with g.fsm
- Output: HA.fsm - Concatenated FSM
conflict
[♦]Tests for non-conflicting languages of the two FSM's.
- File: conflict
- Description: This program tests for non-conflicting languages for the two given FSMs. The machine HG.conf.fsm
contains traces that violate the non-conflicting condition, namely, those in (Lm(H) /\ Lm(G)) \ (Lm(H) /\ Lm(G)) The program requires that both input machines are trim. The program will assume that the machines are accessible and will check if they are co-accessible. If the machines aren't co-accessible. If the machines aren't co-accessible, they are made so and a warning is issued.
- Input:
- H.fsm - Input FSM1
- G.fsm - Input FSM2
- Output: HG_conf..fsm - Conflicting traces
equiv
Tests for the language equivalence of two FSM's.
- File: equiv
- Description: This program tests for the language equivalence of two machines.
- Input:
- H - Input FSM1
- G - Input FSM2
- Output: IF L(H) = L(H) and if Lm(H) = Lm(G).
incl
Tests if L(H) contains L(G) and if Lm(H) contains Lm(G) where H and G are two input FSMs.
- File: incl
- Description: This program tests if L(H1) contains L(H2) and if Lm(H1) contains Lm(H2). The order of input matters.
- Input:
- H1.fsm - Input FSM1
- H2.fsm - Input FSM2
- Output: If L(H1) contains L(H2) and if Lm(H1) contains Lm(H2)
inv_p_L
Returns the inverse projection of the FSM with respect to another one and the given event list.
- File: inv_p_L
- Description: This program creates and returns the inverse projection of L(H) with respect to L(G) and the events in H.events. This is the same as inv_proj (H.fsm, H.events) X G.fsm.
- Input:
- H0.fsm - Input FSM
- G.fsm - Reference FSM
- uc.events - (optional) if used, will override uncontrollable events specified in G.fsm
- Output: H.fsm - Machine representing infimal closed and controllable superlanguage.
inv_proj
[★]Returns the inverse projection of the FSM with respect to the given event list.
- File: inv_proj
- Description: This program creates and returns the inverse projection of L(H) with respect to the given set of events.
- Input:
- H.fsm - Input FSM
- H.events - List of events for inverse projection
- Output: H_inv_fsm - FSM modeling the inverse projection
live
Returns a live FSM given a non-live one by adding self-loops to all DEAD states.
- File: live
- Description: This program creates and returns a live machine given a non-live machine by adding a self-transition "STOP" to any state which has no transitions
- Input: H.fsm - Input FSM
- Output: H_live.fsm - Live FSM
mark_fsm
[★]Marks all the states in the FSM.
- File: mark_fsm
- Description: This program marks all the states in the given FSM
- Input: h.fsm - Input FSM
- Output: h_marked.fsm - Marked FSM
minimize_std
Checks for and removes equivalent states from the FSM using the standard algorithm.
- File: minimize_std
- Description: This program takes an FSM with a completely specified transition function and gives the minimal-state FSM, i.e. equivalent states are merged. The algorithm used is the standard (slow) one found in many introductory textbooks on the subject. If the FSM has a non-total transition function, a slightly modified algorithm is used.
- Input: H.fsm - Input FSM (must be deterministic)
- Output: H_minimal.fsm - Minimum-State FSM
obsvr
Returns observer of the FSM in diagnoser or FSM format.
- File: obsvr
- Description: This program builds the observer for the given FSM. The states in this observer contain the immediate observable reach and unobservable reach of each transition. This observer can be returned in two formats, either the diagnoser format or the FSM format.
- Input: H.fsm - Input FSM
- Output:
- H_obsvr.diag - Observer of H.fsm
- H_obsvr.FSM - (optional) Observer in FSM format
par_comp
Creates the parallel composition of the set of FMS's.
- File: par_comp
- Description: This program creates the synchronous (parallel) composition of a given set of FSMs.
- Input:
- component1.fsm - Input FSM
- component2.fsm - Input FSM2
- ..... - more input FSMs
- Output: sync.fsm - Synchronous FSM
product
[★]Creates the product of two FSM's.
- File: product.c
- Description: This program creates the product of the two given FSMs
- Input:
- component1.fsm - Input FSM1
- component2.fsm - Input FSM2
- Output: sync.fsm - Synchronous FSM
refine
Refines a system model subject to a given speculation model.
- File: refine
- Description: This program refines a given reference FSM G.fsm with respect to a given input FSM H.fsm. It generates output machine Gr, which is a supermachine of H, where L(Gr) = L(G), and Lm(Gr) = Lm(G).
- Input:
- H.fsm - Input FSM
- G.fsm - Reference FSM
- Output: H_refine.fsm - Supermachine of G.fsm
rename_dead
Renames the DEAD state of an FSM to DEADi.
- File: rename_dead
- Description: This program renames the DEAD state of a given FSM to DEADi where i is the smallest integer that makes DEADi a unique state name.
- Input: input.fsm - Input FSM
- Output: output.fsm - Output FSM
rename_states
Renames the states in the FSM, counting up from 1.
- File: rename_states
- Description: This program renames states, counting up from one. FSM h and returns FSM h_rn, which contains the renamed states. It stores the mapping of old names to new names in oldstates.txt for later reference.
- Input: H.fsm - Input FSM
- Output:
- H_rn.fsm - Output FSM
- oldstates.txt - old state names mapped to new names
rm_state
Removes the listed states from the FSM.
- File: rm_state
- Description: This program removes the listed states from the given FSm and returns the new FSM.
- Input:
- h.fsm - Input FSM
- del.states - List of states to delete
- Output: h_del.fsm - machine with the listed states deleted
union
Creates a machine whose language is the union of two FSM's.
- File: union
- Description: This program creates and returns a machine whose generated and marked languages are the union of the languages of the two given FSMs. The order of input matters.
- Input:
- H.fsm - Input FSM1
- G.fsm - Input FSM2
- Output: G_union_G.fsm - Union FSM
Control
coobs
Tests for the coobservability of L(H) with respect to L(G), with two agents.
- File: coobs
- Description: This program tests for the co-observability of L(H) with respect to L(G) and the sets of controllable and observable events specified. The machine m.fsm is built for testing co-observability according to the method of Rudie and Willems.
- Input:
- G.fsm - Reference
- H.fsm - Input FSM
- e1c.events - Controllable events set 1
- e2c.events - Controllable events set 2
- e1o.events - Observable events set 1
- e2o.events - Observable events set 2
- Output: M.fsm - The marked language of this FSM represents the traces that violate coobservability
coobs_gen
General forms of coobs dealing with multiple site and generalized coobservability.
- File: coobs_gen
- Description: This program tests for the co-observability of L(H) with respect to L(G) and the sets of controllable and observable events specified. The machines m and md are built to test for C&P and D&A co-observability, respectively. These FSMs are in turn used to test for generalized co-observability. Any number of agents can be specified.
- Input:
- G.fsm - Reference FSM
- H.fsm - Input FSM
- eNc - List of controllable events for agent N
- eNo - List of observable events for agent N
- Output:
- M.fsm - The marked language of this FSM represents the traces that violate C&P co-observability.
- Md.fsm - The marked language of this FSM represents the traces that violate D&A co-observability.
ctrb
Tests for the controllability of L_m(H) with respect to L(G) and a set of uncontrollable events.
- File: ctrb
- Description: This program tests for the language controllability of a given FSM H with respect to another FSM G and with respect to a set of uncontrollable events. Optionally, the uncontrollable events set may be specified in the .events file which will override specifications in G.
- Input:
- H - Input FSM
- G - Reference FSM
- uc.events - (optional) will override uncontrollable events specified in g.fsm
- Output: If L(H) is controllable with respect to L(G) and the set of uncontrollable events specified.
enable_map
Lists events that are enabled or disables at each state of a supervisor FSM with respect to a system FSM.
- File: enable_map
- Description: Lists events to be enabled/disabled at each state of a supervisor FSM with respect to a system FSM.
- Input:
- G - reference FSM
- H - supremal controllable FSM
- Output: List of events to be enabled and disabled at each state
infcon
Generates the infimal prefix-closed and controllable super-language of a given language with respect to a second prefix-closed language.
- File: infcon
- Description: This function generates a new machine H.fsm that represents the infimal closed and controllable superlanguage of a given language (represented by H0.fsm) with respect to a second closed language (represented by G.fsm).
- Input:
- H0.fsm - Input FSM
- G.fsm - Reference FSM
- uc.events - (optional) if used, will override uncontrollable events specified in G.fsm
- Output: H.fsm - Machine representing infimal closed and controllable superlanguage
normal
Tests for the normality of L(H) with respect to L(G).
- File: normal
- Description: This program tests for the normality of L(H) with respect to L(G) and the set of observable events in G.fsm.
- Input:
- H.fsm - Input FSM
- G.fsm - Reference FSM
- Output: If L(H) is normal with respect to L(G) and the set of observable events in G.fsm
obs
Tests for the observability of L(H) with respect to L(G).
- File: obs
- Description: This program tests for the observability of L(H) with respect to L(G) and the specified sets of controllable and observable events. If event sets are not given, the events in G.fsm are used.
- Input:
- G.fsm - Reference FSM
- H.fsm - Input FSM
- cont.events - (optional) List of controllable events
- obs.events - (optional) list of observable events
- Output: M.fsm - The marked language of this FSM represents the traces that violate observability
supcn
Builds the supremal controllable normal sublanguage of L_m(H) with respect to L(G).
- File: supcn.c
- Description: This language builds the supremal controllable normal sublanguage of the language (non-prefix-closed) marked by H.fsm with respect to G.fsm (and the sets of controllable and observable events in G). \overline(Lm(h_supnorm)) = L(h_supnorm). Note that this does not preserve state names.
- Input:
- H.fsm - Input FSM
- G.fsm - Reference FSM
- Output: H_supcn.fsm - FSM for supremal controllable normal sublanguage (non-prefix-closed)
- Detail: The implemented algorithm implements an iterative algorithm in "A Uniform Approach for Computing Sublanguages Arising in Supervisory Control Theory"
supcn_pc
Builds the supremal controllable normal sublanguage of L(H) with respect to L(G).
- File: supcn.pc
- Description: This program builds the supremal controllable normal sublanguage of the language generated by H.fsm with respect to G.fsm. L(h_supnorm) = L^CN(h) with respect to L(G) and the sets of controllable and observable events in G.fsm. This only works for prefix-closed languages.
- Inputs:
- H.fsm - Input FSM
- G.fsm - Reference FSM
- Output: H_supcn.fsm - FSM for Supremal Controllable Normal sublanguage
- Detail: The following algorithm implements the equation K(sup_cn) = F^(-1) { supcon [ P ( k(supnorm) ) ] } X M)
supcon1
Builds the supremal controllable sublanguage of L_m(H) with respect to L(G).
- File: supcon1
- Description: This program builds a machine, H_sup.fsm, whose marked language is the supremal controllable sub-language of L(H) with respect to L(G) and the given set of uncontrollable events.
- Input:
- H.fsm - Input FSM
- G.fsm - Reference FSM
- uc.events - (optional) if used, will override uncontrollable events specified in g.fsm
- Output: H_sup.fsm - FSM for Supremal Controllable Sublanguage
supcon_std
Builds the supremal controllable sublanguage of L(H) with respect to L(G).
- File: supcon_std
- Description: This program builds a machine, H_sup.fsm, whose marked language is the supremal controllable sublanguage of L_m(H) with respect to L(G) and the set of uncontrollable events in G.fsm.
- Input:
- H.fsm - Input FSM
- G.fsm - Reference FSM
- printf_flag - Specifies option to show the steps of the iterative procedure, namely which states of H are deleted due to the contorllability condition and which are deleted in the trim, at each iteration. Value of 1 will print the steps. Any other value or no value will not.
- Output: H_sup.fsm - FSM representing Supremal Controllable
supnorm
Builds the supremal controllable sublanguage of L_m(H) with respect to L(G).
- File: supnorm
- Description: This program builds the supremal normal sublanguage of the language generated by H.fsm with respect to G.fsm and the set of observable events in G.fsm. L(H_norm) = L(H)^N with respect to L(G) and the set of observable events in G.fsm.
- Input:
- H.fsm - Input FSM
- G.fsm - Reference FSM
- Output: H_norm.fsm - FSM for Supremal Normal Sublanguage
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.
- File: vlp_s
- Description: This program builds a machine, 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 the controllable event set of G. It uses the VLP-S algorithm specified in "Variable Lookahead Supervisory Control with State Information" by Neijb Ben Hadj-Alouane et. al., IEEE Transactions on Automatic Control, Vol 39, No 12, December 1994, pp. 2398-2410.
- Input:
- G.fsm - Reference FSM
- H.fsm - Input FSM
- Output: H.events - List of controllable events in h.fsm
Failure Diagnosis
compose
Generates the composite system with the appropriate sensor readings for each state.
- File: compose
- Description: This program creates and returns the complement of the given FSM, i.e., the language marked by h_comp.fsm is the complement of the language marked by h.fsm with respect to the Kleene closure of the events in h.fsm.
- Input: H.fsm - Input FSM
- Output: H_comp.fsm - Complement FSM
diag
Generates the (multiple fault) diagnoser for the given FSM.
- File: diag
- Description: This program generates the multiple-failure-diagnoser (mf) for the given system. The mf-diagnoser is written into the given output file.
- Input:
- H.fsm - Input FSM
- H.ft - Failure Partition for building diagnoser of H.fsm
- Output:
- Hmf.diag - mf-diagnoser of H.fsm
- H.diag.fsm - (optional) Diagnoser written in FSM format
diag_a
Generates the diagnoser (with ambiguous labels) for the FSM.
- File: diag_a
- Description: This program generates the diagnoser for the given system. The diagnoser is written into the given output file.
- Input:
- H.fsm - Input FSM
- H.ft - Failure Partition for building the diagnoser of H.fsm
- Output:
- H.diag - Diagnoser of H.fsm
- H_diag.fsm - (optional) Diagnoser written in FSM format
diag_EX
Generates the extended diagnoser for the FSM.
- File: diag_EX
- Description: This program generates the multiple-failure-diagnoser (mf-diagnoser) for the given system. The mf-diagnoser is written into the given output file.
- Input:
- H.fsm - Input FSM
- H.ft - Failure Partition for building diagnoser of H.fsm
- Output:
- Hmf.diag - mf-diagnoser of H.fsm
- H.diag.fsm - (optional) Diagnoser written in FSM format
diag_UR
Generates the diagnoser with unobservable reach.
- File: diag_UR
- Description: This program generates the multiple-failure-diagnoser (mf-diagnoser) for the given system. The mf-diagnoser is written into the given output file.
- Input:
- H.fsm - Input FSm
- H.ft- Failure Partition for building diagnoser of H.fsm
- Output:
- Hmf.diag - mf-diagnoser of H.fsm
- H.diag.fsm - (optional) diagnoser written in FSM format
r_cycle
Tests for diagnosability of an intermittent-fault FSM by looking for type o, type i, type p and type r indeterminate cycles.
- File: r_cycle
- Description: This program tests for the diagnosability of the system. It detects 4 different kinds of indeterminate cycles and writes one output file for each cycle type. This deals with machines with intermittant failures.
- Input:
- H.fsm - Input FSM
- H.ft - Failure Partition for building the diagnoser of H.fsm
- Output:
- H.o_cycles - type-o indeterminate cycles in diagnoser
- H.i_cycles - type-i indeterminate cycles in diagnoser
- H.p_cycles - type-p indeterminate cycles in diagnoser
- H.r_cycles - type-r indeterminate cycles in diagnoser
idiag
Generates the I-diagnoser of the FSM.
- File: idiag
- Description: This program generates the I-diagnoser for the given system. The I-diagnoser is written to the given output file.
- Input:
- H.fsm - Input FSM
- H.ft - Failure Partition for building the I-diagnoser of H.fsm
- ind_events.ift - Failure Partition for indicator events
- Output:
- HI.diag - I-diagnoser of H.fsm
- H_diag.fsm - (optional) I-diagnoser written in FSM format
dicycle
Tests for I-diagnosability of the FSM by detecting (Fi,li)-indeterminate cycles.
- File: dicycle
- Description: This program tests for I-diagnosability of the system. It detects (Fi,Ii)-indeterminate cycles in the diagnoser and writes them into the given output file.
- Input:
- H.fsm - Input FSM
- H.ft - Failure Partition for building the I-diagnoser of H.fsm
- ind_events.ift - Failure Partition for indicator events
- Output: HI.cycles - (Fi,Ii)-indeterminate cycles in I-diagnoser
dcycle
Tests for diagnosability of the FSM by detecting Fi-indeterminate cycles.
- File: dcycle
- Description: This program tests for diagnosability (multiple fault) of the system.
- Input:
- H.fsm - Input FSM
- H.ft - Failure Partition for building diagnoser of H.fsm
- Output: Hmf.cycles - Fi-indeterminate cycles in diagnoser
eventmap
Maps the indicator events to the observable states in the FSM.
- File: eventmap
- Description: This program maps the indicator events.ift to the observable states in the system and writes the indicator map to the given ouptut file.
- Input:
- H.obs - List of observable events in H.fsm
- events.ift - List of indicator events
- Output: ind_events.ift - Failure Partition for indicator events
r_diag
Builds a diagnoser that can handle reset events.
- File: r_diag
- Description: This program generates the multiple-failure with reset events-diagnoser (mfr-diagnoser) for the given system. The mfr-diagnoser is written into the given output file.
- Input:
- H.fsm - Input FSM
- H.ft - Failure Partition for building the diagnoser of H.fsm
- Hr.rt - Partition of reset events
- Output:
- Hmf.diag - mf-diagnoser of H.fsm
- H.diag.fsm - (optional) Diagnoser written in FSM format
sensmap
Maps the sensor readings to every state in the FSM.
- File: sensmap
- Description: This program maps the sensor map fsm.map to every state in the given machine and writes the result into the given output file.
- Input:
- h.stats - List of states in h.fsm
- fsm.map - Sensor mapping for some states in h.fsm
- Output: sensor_data.map - Sensor data map
verifier_dia
Builds verifiers to test diagnosibility.
- File: verifier_dia
- Description: Builds verifiers and tests diagnosability of an FSM
- Input:
- H.fsm - Input FSM
- H.ft - Failure Partition for building diagnoser of H.fsm
- Output:
- outN-ver.fsm - the verifier for failure type N
- outN-fc.fsm - the verifier with only the f-confused states
- out.vcycles - lists the f-confused cycles in the verifier
verifier_decen_dia
Builds verifiers to test diagnosibility in a decentralized system.
- File: verifier_decen_dia
- Description: This program creates decentralized verifiers for L(G) and tests decentralized diagnosability. One decentralized verifier is created for each failure type to reduce computational complexity. Any number of agents can be supplied. If L(G) is not decentralized diagnosable, it returns failure confused cycles.
- Input:
- n_agents - how many agents will observe events
- Sys.fsm - System FSM
- Sys.ft - Failure Partition file for verifiers
- agent1.o to agentN.o - observable event files for each agent
- out - base name for output verifiers
- Output:
- out-.fsm - A verifier for each failure type
- out-.vcycles - list of confused cycles for each failure type
Stochastic Diagnosability
a_diagnosability
Tests for A-Diagnosability by looking at the given FSM's stochastic diagnoser.
- File: a_diagnosability
- Description: This program generates a stochastic diagnoser and uses it to test for A-Diagnosability.
- Input:
- H.fsm - Input FSM
- H.stoc- Stochastic information for FSM
- H.ft - Failure Partition for building diagnoser of H.fsm
- out.txt - Output for command line version
- Output: Whether H.fsm is A-Diagnosable or not
create_sfsm
Interactive routine to create stochastic information files for an existing FSM.
- File: create_sfsm
- Description: This program guides the user through creating a stochastic file for an existing Finite State Machine.
- Input: H.fsm
- Output: H.stoc
- Detail: An FSM needs to have a .stoc file in order to run any Stochastic methods (like A-Diagnosability).
sdiag
Generates the stochastic diagnoser for the given FSM.
- File: s_diag
- Description: Command-line simplified output diagnoser routine. In the simplified diagnoser format, just the ID no., certain and uncertain attribute fields, and next events/states are outputted. The list of state, label pairs is removed.
- Input:
- H.fsm - Input FSM
- H.ft - Failure Partition for building a diagnoser of h.fsm
- Output:
- H.sdiag - Diagnoser of Hf.fsm in a simplified format
- H_diag.fsm - (optional) Diagnoser written in FSM format