Skip to content

GitLab

Last edited by Sebastian Uchitel
Page history

Modal Transition Systems

Modal Transition Systems

The tool, as its name suggests support model checking and synthesis using modal transition systems. This functionality has not received attention in many years and may not be fully functional.

component

The component keyword is intended to build a Modal Transition System (MTS) component by projecting a composed system onto a given interface alphabet (the actions listed after |), abstracting away the rest of the behaviour:

component ||NAME = (P || Q) | {interfaceActions}.

The optimistic and pessimistic keywords are MTS refinement operations, applied as a prefix to a modal model:

  • optimistic — the optimistic model: the maximal implementation, treating maybe transitions as present, e.g. optimistic ||M = (...).
  • pessimistic — the dual pessimistic model: the minimal implementation, dropping maybe transitions and keeping only required behaviour.

Other Modal Transition System and scenario keywords, not yet documented:

  • restricts — scenario restriction
  • instances — scenario instances
  • condition — a named Fluent Propositional Logic predicate used inside triggered scenarios (eTS/uTS), referenced by the pre/main charts.
  • prechart — prechart in a triggered scenario
  • mainchart — main chart in a triggered scenario
  • eTS — existentially triggered scenario
  • uTS — universally triggered scenario
  • starenv — star environment
  • buchi — Büchi automaton specification

Abstract

The abstract keyword builds a Modal Transition System (MTS) from the LTS resulting from compiling an FSP process, adding a may transition for every label that is disabled (not enabled) in a state. The keyword can be used with sequential and composite processes.

abstract LOWER = (a -> b -> LOWER).

LOWER = (a -> b -> LOWER).
abstract ||PL = (LOWER)\{a}.

Modal transition systems (MTS) can be modelled by using a question mark (?) on event labels to indicate may-transitions (transitions that may or may not be present in an implementation).

A = (a -> b? -> A | a? -> A).

Abstract keyword

The abstract keyword builds an MTS from an FSP process by adding to each state maybe-transitions on labels that are not enabled in the original process. It can be applied both to sequential and composite processes.

abstract A = (a -> b -> A | a->STOP | b->END).

B = (a -> b -> B | b? -> B).
abstract ||COMP = (B).

← End User