# DESUMA2 Functions

DESUMA2 Functions
 Revision as of 17:22, August 1, 2013 (view source)Drotarov (Talk | contribs)← Older edit Revision as of 17:03, August 2, 2013 (view source)Drotarov (Talk | contribs) Newer edit → Line 99: Line 99: :-Select '''Inverse Projection to L'''. :-Select '''Inverse Projection to L'''. :-Select the two FSMs, then open the file browser to select the event list. :-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. :-Click submit.

## Revision as of 17:03, August 2, 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.

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