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.

Contents 1 Manipulation 1.1 Accessibility 1.2 Co-Accessibility 1.3 Complement FSM 1.4 Concatenation 1.5 Conflict 1.6 Equivalent 1.7 Inclusion 1.8 Inverse Projection to L 1.9 Inverse Projection 1.10 Minimum State FSM 1.11 Observer 1.12 Parallel Composition 1.13 Product 1.14 Refine 1.15 Trim 1.16 Union 2 Control 2.1 Coobservability 2.2 Controllability 2.3 Infimal Controllable Superlanguage 2.4 Normality 2.5 Observability 2.6 Supremal Controllable Normal Sublanguage 2.7 Supremal Controllable Normal Sublanguage (prefix-closed case) 2.8 Supremal Controllable Sublanguage 2.9 Supremal Controllable Sublanguage (Variable Lookahead) 3 Diagnosis 3.1 Diagnoser 3.2 Diagnoser with unobservable reach 3.3 Dcycle 3.4 Verifier

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.