|
|
# LTS-JSON-Specification
|
|
|
|
|
|
This is a specification of the pseuCo.com-LTS-JSON-format, version 1.1.
|
|
|
|
|
|
## General
|
|
|
|
|
|
Every state in the LTS is represented by a unique *label* of type *string*.
|
|
|
|
|
|
Every LTS is represented by a valid JSON string, as specified on http://json.org/. The object represented by this JSON string has two mandatory properties:
|
|
|
|
|
|
- `initialState`, the label of the initial state.
|
|
|
- `states`, the state map.
|
|
|
|
|
|
The object may contain additional properties which must be ignored.
|
|
|
|
|
|
## State Map
|
|
|
|
|
|
The state map is an object describing the states and transitions. Each state in the LTS corresponds to a property of this object, whose key is the label of the state. The value of such a property is an object containing an array of transition objects under the key `transitions`.
|
|
|
|
|
|
## Transition object
|
|
|
|
|
|
A transition object is an object having the following properties:
|
|
|
|
|
|
- `target`, the string label of the target state.
|
|
|
- `detailsLabel`, either a string containing additional details (e.g. for a τ-transition: the action that caused the synchronization), or the boolean value `false`, indicating that no additional label is available. This property is optional.
|
|
|
- Either `label`, a string containing the label (e.g. the action) of the transition, or `weak` with the value `true`, to signal that a transition is weak. For legacy reasons, a transition may have both properties, where `label` is ignored.
|
|
|
|
|
|
The transition object does not contain the source state of the transition. Instead, this object is only used in a context where the source state is fixed.
|
|
|
|
|
|
The object may contain additional properties which must be ignored.
|
|
|
|
|
|
# Example
|
|
|
|
|
|
The LTS created by the CCS term `a.b.0 + i.0` (remember that `i` in CCS represents a τ-transition) can be represented by this string:
|
|
|
|
|
|
```
|
|
|
{
|
|
|
"initialState": "a.b.0 + τ.0",
|
|
|
"states": {
|
|
|
"0": {
|
|
|
"transitions": []
|
|
|
},
|
|
|
"a.b.0 + τ.0": {
|
|
|
"transitions": [
|
|
|
{
|
|
|
"weak": true,
|
|
|
"detailsLabel": false,
|
|
|
"target": "b.0"
|
|
|
},
|
|
|
{
|
|
|
"label": "τ",
|
|
|
"detailsLabel": false,
|
|
|
"target": "0"
|
|
|
}
|
|
|
]
|
|
|
},
|
|
|
"b.0": {
|
|
|
"transitions": [
|
|
|
{
|
|
|
"label": "b",
|
|
|
"detailsLabel": false,
|
|
|
"target": "0"
|
|
|
}
|
|
|
]
|
|
|
}
|
|
|
}
|
|
|
}
|
|
|
``` |
|
|
\ No newline at end of file |