DESUMA2 Functions

From DESUMA Wiki
DESUMA2 Functions
Jump to: navigation, search
Line 195: Line 195:
 
:-Select '''Union'''.
 
:-Select '''Union'''.
 
:-Select the desired FSMs.
 
:-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.
 
:-Click submit.

Revision as of 19:51, August 5, 2013

This tutorial page for DESUMA and UMDES focuses on the use of the UMDES operations on automata.

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.

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

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

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