The modal logic controlled system synthesis application takes a CIF
specification with plant automata containing discrete and continuous
variables, and a modal logic formula as requirement, and constructs a
controlled system state space by interpreting the CIF specification in an
untimed manner. The resulting state space is *safe*, in the sense that the
requirement is fulfilled in each state. It is *controllable* in the sense that
no edge with an uncontrollable event in the controlled system will lead to a
state outside the state space. Finally, it is *maximal*, in the sense that
there are no safe and controllable states that are not in the resulting state
space.

The modal logic synthesis algorithm is based on the following paper: A.C. van Hulst, M.A. Reniers, and W.J. Fokkink: Maximally Permissive Controlled System Synthesis for Modal Logic, SOFSEM 2015, 41st International Conference on Current Trends in Theory and Practice of Computer Science, January 24-29, 2015, Pec pod Sněžkou, Czech Republic. To appear in Lecture Notes in Computer Science, 2015.

The transformation can be started in the following ways:

- In Eclipse, right click a
`.cif`file in the*Project Explorer*or*Package Explorer*and choose*CIF synthesis tools ‣ Apply modal logic synthesis...*. - In Eclipse, right click an open text editor for a
`.cif`file and choose*CIF synthesis tools ‣ Apply modal logic synthesis...*. - Use the
`cif3modallogic`tool in a ToolDef 2 script. See the*scripting documentation*and*tools overview*page for details. - Use the
`cif3modallogic`*command line tool*.

*Input file path*: The absolute or relative local file system path to the input CIF specification.*Modal logic formula*: The requirements formula to apply to the CIF specification. For details, see the*syntax of the modal logic formula*for further details.*Output file path*: The absolute or relative local file system path to the output CIF file. See also*specifying the CIF output file*below for further details.*Enable CIF*: If set, write a CIF output file. See also*specifying the CIF output file*below for further details.*Report file path*: The absolute or relative local file system path to the output report file. See also*specifying the report output file*below for further details.*Enable report*: If set, write a report output file. See also*specifying the report output file*below for further details.

In the modal logic formula, the requirements of the controlled system are expressed. Its syntax is:

p::= "marked" | "deadlock" | "true" | "false" | `boolean variable` | `automaton location` | | "<"event">" "true" "not" p | p "or" p | p "and "p" | p "=>" p | p "<=>" pf::= p | "["event"]" f | "<"event">" f | "[]" f | "<>" f p "or" f | f "and f"

Elementary boolean properties are expressed as `p`. They often take the form
or an algebraic or discrete boolean variable, or the name of a location in an
automaton. There are also three properties that are very useful for defining a
supervised system, namely `marked` (which holds if the combined automata
state is marked), `deadlock` (which holds when a combined automata state
has no outgoing transitions), and `< e > true` (which holds when there is an
outgoing edge with event `e`). Note that the latter is a special case of the
generic `< e > f` formula discussed below. Since this form is a property
rather than a formula, it is allowed at more places in the modal logic
formula. You can apply `not`, `and`, `or`, `=>`, and `<=>`
operations on these properties to construct arbitrary complex boolean
expressions over the state.

The formula `f` is a layer on top of the boolean expressions, that defines
when the expression should hold. If it is a `p`, the `p` expression must
hold in the current state. The `[ e ] f` and `< e > f` formulas require
`f` to hold in the next state, after event `e`. The former (`[ e ] f`)
demands formula `f` must hold after each edge with event `e` from the
current state. The latter (`< e > f`) is a weaker requirement, one next
state after an edge with event `e` is sufficient then. The `[] f`
expresses that `f` must always hold (for the current state, and every future
state), while `<> f` means that `f` must hold now or in a future state.

The `p or f` allows to combine a property `p` with a formula `f`, where
at least one of them must hold. Finally, the `f and f` rule allows
strengthening of the formula, since both sides of the `and` must hold.

If the *Output file path* option has a value or the *Enable CIF* option is
set, a CIF output file is written containing the state space of the controlled
system.

The filename used for the output file is given in the *Output file path*
option, if provided. Otherwise, the input CIF file path is used, where
the `.cif` file extension is removed (if present), and a `_ctrlsys.cif`
file extension is added.

If the *Report file path* option has a value or the *Enable report* option is
set, a report file is written containing details of the state space of the
generated controlled system.

The filename used for the report file is given in the *Report file path*
option, if provided. Otherwise, the input CIF file path is used, where
the `.cif` file extension is removed (if present), and a `_report.txt`
file extension is added.

The modal logic synthesis tool supports a subset of CIF specifications. The following restrictions apply:

- Only plant and kindless/regular automata (without a supervisory kind) are supported.
- Only plant and kindless/regular invariants (without a supervisory kind) are supported.
- Usage of distribution types is not supported.
- Usage of function types is not supported.
- Function calls (both to user-defined functions and to standard library functions) are not supported.
- Usage of derivatives is not supported.
- User-defined functions are not supported.
- Input variables are not supported.
- Specifications with more than 2
^{31}- 1 = 2,147,483,647 potential initial states are not supported.

The following *CIF to CIF transformations* are
applied as preprocessing (in the given order), to increase the subset of CIF
specifications that can be synthesized:

*Remove I/O declarations**Eliminate component definition/instantiation**Eliminate automaton self references*

In addition it applies the
*Simplify values (no references, optimized)* CIF to CIF
transformation to speed up processing.