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.

Contents 1 Input/Output Routines 1.1 create_fsm 1.2 forbid 1.3 write_ev 1.4 write_o 1.5 write_st 1.6 write_uo 2 Manipulation of FSM 2.1 acc 2.2 change_cprop 2.3 change_initial_state 2.4 change_oprop 2.5 c_par_comp 2.6 co_acc 2.7 comp_fsm 2.8 concat 2.9 concat_ev 2.10 conflict 2.11 equiv 2.12 incl 2.13 inv_p_L 2.14 inv_proj 2.15 live 2.16 mark_fsm 2.17 minimize_std 2.18 obsvr 2.19 par_comp 2.20 product 2.21 refine 2.22 rename_dead 2.23 rename_states 2.24 rm_state 2.25 union 3 Control 3.1 coobs 3.2 coobs_gen 3.3 ctrb 3.4 enable_map 3.5 infcon 3.6 normal 3.7 obs 3.8 supcn 3.9 supcn_pc 3.10 supcon1 3.11 supcon_std 3.12 supnorm 3.13 vlp_s 4 Failure Diagnosis 4.1 compose 4.2 diag 4.3 diag_a 4.4 diag_EX 4.5 diag_UR 4.6 r_cycle 4.7 idiag 4.8 dicycle 4.9 dcycle 4.10 eventmap 4.11 r_diag 4.12 sensmap 4.13 verifier_dia 4.14 verifier_decen_dia 5 Stochastic Diagnosability 5.1 a_diagnosability 5.2 create_sfsm 5.3 sdiag

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