UMDES Commands

From DESUMA Wiki
UMDES Commands
Jump to: navigation, search

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

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.

Threshold - Failure threshold
Component1.map - First failure map
Component2.map - Second failure map
...- more maps


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 inaccessible states from the FSM.


change_cprop

Changes controllability properties of events.

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.
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)


change_initial_state

Change the initial state of the FSM.

A.fsm - Input FSM
state_name - Name of state in A.fsm to be initial state


change_oprop

Changes observability properties of events.

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.
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)


c_par_comp

Creates the constrained parallel composition of the set of FSMs.

Number of Machines
forbid.states - Set of forbidden states
component1.fsm - Input FSM 1
.... - more input FSMs


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.

G.fsm - First FSM
H.fsm - Second FSM

concat_ev

Adds transitions to the DEAD state for all events in the event list.

H.fsm - Input FSM
A.events - List of events to be concatenated with g.fsm


conflict

[♦]Tests for non-conflicting languages of the two FSM's.

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.

H.fsm - Input FSM1
G.fsm - Input FSM2


equiv

Tests for the language equivalence of two FSM's.

H - Input FSM1
G - Input FSM2


incl

Tests if L(H) contains L(G) and if Lm(H) contains Lm(G) where H and G are two input FSMs.

H1.fsm - Input FSM1
H2.fsm - Input FSM2


inv_p_L

Returns the inverse projection of the FSM with respect to another one and the given event list.

H0.fsm - Input FSM
G.fsm - Reference FSM
uc.events - (optional) if used, will override uncontrollable events specified in G.fsm


inv_proj

[★]Returns the inverse projection of the FSM with respect to the given event list.

H.fsm - Input FSM
H.events - List of events for inverse projection


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

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.

component1.fsm - Input FSM
component2.fsm - Input FSM2
..... - more input FSMs


product

[★]Creates the product of two FSM's.

component1.fsm - Input FSM1
component2.fsm - Input FSM2


refine

Refines a system model subject to a given speculation model.

H.fsm - Input FSM
G.fsm - Reference FSM


rename_dead

Renames the DEAD state of an FSM to DEADi.


rename_states

Renames the states in the FSM, counting up from 1.

H_rn.fsm - Output FSM
oldstates.txt - old state names mapped to new names


rm_state

Removes the listed states from the FSM.

h.fsm - Input FSM
del.states - List of states to delete


union

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

H.fsm - Input FSM1
G.fsm - Input FSM2


Control

coobs

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

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


coobs_gen

General forms of coobs dealing with multiple site and generalized coobservability.

G.fsm - Reference FSM
H.fsm - Input FSM
eNc - List of controllable events for agent N
eNo - List of observable events for agent N
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.

H - Input FSM
G - Reference FSM
uc.events - (optional) will override uncontrollable events specified in g.fsm


enable_map

Lists events that are enabled or disables at each state of a supervisor FSM with respect to a system FSM.

G - reference FSM
H - supremal controllable FSM


infcon

Generates the infimal prefix-closed and controllable super-language of a given language with respect to a second prefix-closed language.

H0.fsm - Input FSM
G.fsm - Reference FSM
uc.events - (optional) if used, will override uncontrollable events specified in G.fsm


normal

Tests for the normality of L(H) with respect to L(G).

H.fsm - Input FSM
G.fsm - Reference FSM


obs

Tests for the observability of L(H) with respect to L(G).

G.fsm - Reference FSM
H.fsm - Input FSM
cont.events - (optional) List of controllable events
obs.events - (optional) list of observable events


supcn

Builds the supremal controllable normal sublanguage of L_m(H) with respect to L(G).

H.fsm - Input FSM
G.fsm - Reference FSM


supcn_pc

Builds the supremal controllable normal sublanguage of L(H) with respect to L(G).

H.fsm - Input FSM
G.fsm - Reference FSM


supcon1

Builds the supremal controllable sublanguage of L_m(H) with respect to L(G).

H.fsm - Input FSM
G.fsm - Reference FSM
uc.events - (optional) if used, will override uncontrollable events specified in g.fsm


supcon_std

Builds the supremal controllable sublanguage of L(H) with respect to L(G).

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.


supnorm

Builds the supremal controllable sublanguage of L_m(H) with respect to L(G).

H.fsm - Input FSM
G.fsm - Reference FSM


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.

G.fsm - Reference FSM
H.fsm - Input FSM

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.

H.fsm - Input FSM
H.ft - Failure Partition for building diagnoser of H.fsm
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.

H.fsm - Input FSM
H.ft - Failure Partition for building the diagnoser of H.fsm
H.diag - Diagnoser of H.fsm
H_diag.fsm - (optional) Diagnoser written in FSM format


diag_EX

Generates the extended diagnoser for the FSM.

H.fsm - Input FSM
H.ft - Failure Partition for building diagnoser of H.fsm
Hmf.diag - mf-diagnoser of H.fsm
H.diag.fsm - (optional) Diagnoser written in FSM format


diag_UR

Generates the diagnoser with unobservable reach.

H.fsm - Input FSm
H.ft- Failure Partition for building diagnoser of H.fsm
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.

H.fsm - Input FSM
H.ft - Failure Partition for building the diagnoser of H.fsm
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.

H.fsm - Input FSM
H.ft - Failure Partition for building the I-diagnoser of H.fsm
ind_events.ift - Failure Partition for indicator events
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.

H.fsm - Input FSM
H.ft - Failure Partition for building the I-diagnoser of H.fsm
ind_events.ift - Failure Partition for indicator events


dcycle

Tests for diagnosability of the FSM by detecting Fi-indeterminate cycles.

H.fsm - Input FSM
H.ft - Failure Partition for building diagnoser of H.fsm


eventmap

Maps the indicator events to the observable states in the FSM.

H.obs - List of observable events in H.fsm
events.ift - List of indicator events


r_diag

Builds a diagnoser that can handle reset events.

H.fsm - Input FSM
H.ft - Failure Partition for building the diagnoser of H.fsm
Hr.rt - Partition of reset events
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.

h.stats - List of states in h.fsm
fsm.map - Sensor mapping for some states in h.fsm


verifier_dia

Builds verifiers to test diagnosibility.

H.fsm - Input FSM
H.ft - Failure Partition for building diagnoser of H.fsm
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.

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

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


create_sfsm

Interactive routine to create stochastic information files for an existing FSM.


sdiag

Generates the stochastic diagnoser for the given FSM.

H.fsm - Input FSM
H.ft - Failure Partition for building a diagnoser of h.fsm
H.sdiag - Diagnoser of Hf.fsm in a simplified format
H_diag.fsm - (optional) Diagnoser written in FSM format
Personal tools
Namespaces
Variants
Actions
Navigation
Toolbox
EECS @ UM
Tools