DESUMA2 Functions

From DESUMA Wiki
DESUMA2 Functions
Jump to: navigation, search

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

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.
Personal tools
Namespaces
Variants
Actions
Navigation
Toolbox
EECS @ UM
Tools