Sublibrary LogicalFunctions contains operators without memory, implemented as Modelica functions. The input arguments of these functions have 2-valued logic type (Boolean). The output arguments of these functions have 2-valued or 3-valued logic type (Boolean or Property). The provided operators reason about their input arguments based on Boolean algebra. The icon of a function depends on the the type of its output argument (whether it is Boolean or Property).
| Name | Description |
|---|---|
| card | Returns the number of elements of a Boolean vector that are true |
| exists | Returns true if at least one element of a Boolean vector is true ('or' of all elements) |
| forall | Returns true if all elements of a Boolean vector are true ('and' of all elements) |
| implies | Returns check as long as the condition is true, otherwise returns true |
| first | Returns the value of the first element of a Boolean vector |
| last | Returns the value of the last element of a Boolean vector |
| oneTrue | Returns true if exactly one element of a Boolean vector is true ('xor' of all elements) |
| PropertyToBoolean | Convert Property (Violated, Undecided, Satisfied) to Boolean (false, true) |
| PropertyToInteger | Convert Property (Violated, Undecided, Satisfied) to Integer (1,2,3) |
| BooleanToProperty | Convert Boolean (false,true) to Property (Violated, Satisfied) |
| IntegerToProperty | Convert Integer (1,2,3) to Property (Violated, Undecided, Satisfied) |
| during | Return Satisfied when check is true as long as condition is true |
| during3 | Return Satisfied when check is Satisfied as long as condition is true (check: 3-valued logic) |
| forall3 | Returns Violated, if at least one element of the Property vector is Violated (vector: 3-valued logic) |
| cardSatisfied | Returns the number of elements of a Property vector that are Satisfied |
| cardUndecided | Returns the number of elements of a Property vector that are Undecided |
| cardViolated | Returns the number of elements of a Property vector that are Violated |