|
|
|
Modal transition systems (MTS) can be modelled by using a question mark (?) on event labels.
|
|
|
|
# Modal Transition Systems
|
|
|
|
|
|
|
|
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 a FSP process adding to each state maybe
|
|
|
|
transitions on labels that are not enabled in the original process.
|
|
|
|
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.
|
|
|
|
|
|
|
|
```
|
| ... | ... | @@ -15,7 +17,5 @@ B = (a -> b -> B | b? -> B). |
|
|
|
abstract ||COMP = (B).
|
|
|
|
```
|
|
|
|
|
|
|
|
# End
|
|
|
|
|
|
|
|
---
|
|
|
|
[← End User](End-User) |
|
|
\ No newline at end of file |
|
|
|
[← End User](End-User) |