DESUMA2 Functions
This tutorial page for DESUMA and UMDES focuses on the use of the UMDES operations on automata.
Note: These functions can be found under the Umdes drop-down menu on the main toolbar of DESUMA.
For a full list of all UMDES functions and how to use them, visit the UMDES Commands page.
Manipulation
Accessibility
Removes any inaccessible states from input automaton.
Requires: one input automaton.
Use:
- Open Manipulation under the Umdes drop-down menu.
- Select Accessibility.
- Check the automaton desired.
- Click submit.
Co-Accessibility
Returns co-accessible part of input automaton.
Requires: one input automaton.
Use:
- Open Manipulation under the Umdes drop-down menu.
- Select Co-Accessibility.
- Check the automaton desired.
- Click submit.
Complement FSM
Returns the complement of the input automaton.
Requires: one input automaton.
Use:
- Open Manipulation under the Umdes drop-down menu.
- Select Complement FSM
- Check the automaton desired.
- Click submit.
Concatenation
Returns the concatenation of two input automata.
Requires: two input automata.
Use:
- Open Manipulation under the Umdes drop-down menu.
- Select Concatenation.
- Select the two automata desired.
- Click submit.
Conflict
Tests for non-conflicting languages of two automata.
Requires: two input automata.
Use:
- Open Manipulation under the Umdes drop-down menu.
- Select Conflict.
- Check the two automata desired.
- Click submit.
Equivalent
Tests for language equivalency of two FSMs.
Requires: two input FSMs.
Use:
- Open Manipulation under the Umdes drop-down menu.
- Select Equivalent
- Check the two FSMs desired.
- Click submit.
Inclusion
Tests if L(H) contains L(G) and Lm(H) contains Lm(G).
Requires: two input FSMs, H and G.
Use:
- Open Manipulation under the Umdes drop-down menu.
- Select Inclusion.
- In order, select FSM H, then select FSM G.
- Click submit.
Inverse Projection to L
Returns the inverse projection of a FSM with respect to another FSM and a given event list.
Requires: two input FSMs, H and G, and an event list.
Use:
- Open Manipulation under the Umdes drop-down menu.
- Select Inverse Projection to L.
- Select the two FSMs, then open the file browser to select the event list.
- Click submit.
Inverse Projection
Returns the inverse projection of the given FSM with respect to a given event list.
Requires: one input FSM and an event list.
Use:
- Open Manipulation under the Umdes drop-down menu.
- Select Inverse Projection.
- Select the FSM and event list.
- Click submit.
Minimum State FSM
Checks for and removes equivalent from FSM using the standard algorithm.
Requires: one input FSM.
Use:
- Open Manipulation under the Umdes drop-down menu.
- Select Minimum State FSM.
- Select the FSM desired.
- Click submit.
Observer
Builds an observer for input FSM.
Requires: one input FSM.
Use:
- Open Manipulation under the Umdes drop-down menu.
- Select Observer.
- Select the FSM desired.
- Click submit.
Parallel Composition
Builds the parallel composition for n number of FSMs.
Requires: at least two input FSMs.
Use:
- Open Manipulation under the Umdes drop-down menu.
- Select Parallel Composition.
- Select the desired FSMs.
- Click submit.
Product
Creates the product of two FSMs.
Requires: two input FSMs.
Use:
- Open Manipulation under the Umdes drop-down menu.
- Select Product.
- Select the desired FSMs.
- Click submit.
Refine
Refines a system model subject to a given specification model.
Requires: one input FSM.
Use:
- Open Manipulation under the Umdes drop-down menu.
- Select Refine.
- Select the desired FSM.
- Click submit.
Trim
Returns the accessible and co-accessible part of an FSM.
Requires: one input FSM.
Use:
- Open Manipulation under the Umdes drop-down menu.
- Select Trim.
- Select the desired FSM.
- Click submit.
Union
Creates a FSM whose language is the union of two FSMs.
Requires: two input FSMs.
Use:
- Open Manipulation under the Umdes drop-down menu.
- Select Union.
- Select the desired FSMs.
- Click submit.
Control
Coobservability
Tests the coobservability of L(H) with respect to L(G) with two agents. First you select H, then G.
Requires: two input FSMs and 4 agent files.
Use:
- Open Control under the Umdes drop-down menu.
- Select Coobservability.
- Select the two FSMs in the order of H and G. Then select the 4 observable event files.
- Click submit.
Controllability
Checks if Lm_(H) is controllable with respect to L(H) and E{uc}. Select H first, then G.
Requires: two input FSMs and one event agent.
Use:
- Open Control under the Umdes drop-down menu.
- Select Controllability.
- Select the two FSMs in the order of H and G. Then select the event agent.
- Click submit.
Infimal Controllable Superlanguage
Creates the infimal prefix closed and controllable superlanguage of L(H) with respect to L(G). Select H, then G.
Requires: two FSMs and an event file.
Use:
- Open Control under the Umdes drop-down menu.
- Select Infimal Controllable Superlanguage.
- Select the two FSMs in order of H and G. Then select the event file.
- Click submit.
Normality
Checks if L(H) is normal with respect to L(G). Select H, then G.
Requires: two input FSMs.
Use:
- Open Control under the Umdes drop-down menu.
- Select Normality.
- Select the two FSMs in order.
- Click submit.
Observability
Tests for the observability of L(H) with respect to L(G). Select H, then G.
Requires: two input FSMs.
Use:
- Open Control under the Umdes drop-down menu.
- Select Observability.
- Select the two FSMs in the order of H and G.
- Click submit.
Supremal Controllable Normal Sublanguage
Creates the supremal controllable normal sublanguage of Lm_(H) with respect to L(G). Select H, then G.
Requires: two input FSMs.
Use:
- Open Control under the Umdes drop-down menu.
- Select Supremal Controllable Normal Sublanguage.
- Select the two FSMs in the order of H and G.
- Click submit.
Supremal Controllable Normal Sublanguage (prefix-closed case)
Creates the supremal controllable normal sublanguage of L(H) with respect to L(G). Select H, then G.
Requires: two input FSMs and an uncontrollable event file.
Use:
- Open Control under the Umdes drop-down menu.
- Select Supremal Controllable Normal Sublanguage (Prefix-closed case) .
- Select the two FSMs in the order of H and G. Also, select the uncontrollable event file.
- Click submit.
Supremal Controllable Sublanguage
Creates the supremal controllable sublanguage of Lm_(H) with respect to L(G). Select H, then G.
Requires: two input FSMs.
Use:
- Open Control under the Umdes drop-down menu.
- Select Supremal Controllable Sublanguage.
- Select the two FSMs in the order of H and G.
- Click submit.
Supremal Controllable Sublanguage (Variable Lookahead)
Creates the supremal controllable sublanguage of the intersection of Lm_(H) with Lm_(G) with respect to L(G) using a variable lookahead algorithm. Select H, then G.
Requires: two input FSMs.
Use:
- Open Control under the Umdes drop-down menu.
- Select Supremal Controllable Sublanguage (variable lookahead).
- Select the two FSMs in the order of H and G.
- Click submit.
Diagnosis
Diagnoser
Generates the multiple failure (mf)-diagnoser for the system.
Requires: one input FSM, one failure partition file, and output specification.
Use:
- Open Diagnosis under the Umdes drop-down menu.
- Select Diagnoser.
- Select the FSM and the failure partition file.
- Specify output parameters.
- Click submit.
Diagnoser with unobservable reach
Generates the multiple failure (mf)-diagnoser for the system.
Requires: one input FSM, one failure partition file, and output specification.
Use:
- Open Diagnosis under the Umdes drop-down menu.
- Select Diagnoser with unobservable reach.
- Select the FSM and the failure partition file.
- Specify output parameters.
- Click submit.
Dcycle
Tests for diagnosability of FSM by detecting Fi-intermediate cycles.
Requires: one FSM and one failure partition file.
Use:
- Open Diagnosis under the Umdes drop-down menu.
- Select Dcycle.
- Select the FSM and failure partition file.
- Click submit.
Verifier
Builds verifiers and tests diagnosability of FSMs.
Requires: one input FSM and one failure partition file.
Use:
- Open Diagnosis under the Umdes drop-down menu.
- Select Verifier.
- Select the FSM and failure partition file.
- Click submit.