# UMDES Commands

Line 27: | Line 27: | ||

[[change_cprop]]: Changes controllability properties of events. | [[change_cprop]]: Changes controllability properties of events. | ||

− | [ | + | [[change_initial_state]]: Change the initial state of the FSM. |

− | [ | + | [[change_oprop]]: Changes observability properties of events. |

− | [ | + | [[c_par_comp]]: Creates the constrained parallel composition of the set of FSMs. |

− | [X][O] [ | + | [X][O] [[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. |

− | [O] [ | + | [O] [[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. |

− | [X] [ | + | [X] [[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. |

− | [X] [ | + | [X] [[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 observer of the FSM in diagnoser or FSM format. |

− | [ | + | [[par_comp]]: Creates the parallel composition of the set of FMS's. |

− | [X] [ | + | [X] [[product]]: Creates the product of two FSM's. |

− | [ | + | [[refine]]: Refines a system model subject to a given speculation 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. |

− | [ | + | [[union]]: Creates a machine whose language is the union of two FSM's. |

== Control == | == Control == | ||

− | [ | + | [[coobs]]: Tests for the coobservability of L(H) with respect to L(G), with two agents. |

− | [ | + | [[coobs_gen]]: General forms 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 disables 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 sublanguage 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 == | == 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 diagnosability 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-diagnosability of the FSM by detecting (Fi,li)-indeterminate cycles. |

− | [ | + | [[dcycle]]: Tests for diagnosability 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 diagnosibility. |

− | [ | + | [[verifier_decen_dia]]: Builds verifiers to test diagnosibility in a decentralized system. |

== Stochastic Diagnosability == | == 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. |

## Revision as of 18:59, July 29, 2013

Commands for UMDES software, when used from the command line, are listed here.

Historical note: UMDES uses the terminology FSM (finite state machine) instead of FSA.

If denoted by [X], the command accepts NDFM (nondeterministic finite state machines) with EMPTY_TRACE transitions.

If denoted by [O], click the command for detailed information and examples. TODO!

## Contents |

## 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

[X][O] acc: Removes inaccessible states from the FSM.

change_cprop: Changes controllability properties of events.

change_initial_state: Change the initial state of the FSM.

change_oprop: Changes observability properties of events.

c_par_comp: Creates the constrained parallel composition of the set of FSMs.

[X][O] 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.

[O] 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.

[X] 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.

[X] 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 observer of the FSM in diagnoser or FSM format.

par_comp: Creates the parallel composition of the set of FMS's.

[X] product: Creates the product of two FSM's.

refine: Refines a system model subject to a given speculation 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.

union: Creates a machine whose language is the union of two FSM's.

## Control

coobs: Tests for the coobservability of L(H) with respect to L(G), with two agents.

coobs_gen: General forms 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 disables 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 sublanguage 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 diagnosability 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-diagnosability of the FSM by detecting (Fi,li)-indeterminate cycles.

dcycle: Tests for diagnosability 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 diagnosibility.

verifier_decen_dia: Builds verifiers to test diagnosibility 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.