Skip to content

Commit 5858200

Browse files
clayratAndré Videla
clayrat
authored and
André Videla
committed
Add option to support both petrinets and finite state machines
1 parent fcf787a commit 5858200

File tree

13 files changed

+341
-171
lines changed

13 files changed

+341
-171
lines changed

‎README.md‎

Lines changed: 222 additions & 58 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
# Statebox's FSM-Oracle
22

3-
A formally verified idris program that evaluates executions for finite state machines (FSM).
3+
A formally verified idris program that evaluates executions for finite state machines (FSM) and Petri nets.
44

5-
The program uses the input provided in `FSMSpec` (see below) to build the underlying graph of the FSM, and generates the free category on it using [idris-ct](https://github.com/statebox/idris-ct/). It then uses the initial state and path provided in the execution (call them `x` and `[x1, ... , xn]`, respectively) to evaluate the composition `idx;x1;...;xn`. It returns success or error depending if this defines a valid morphism in the free category or not.
5+
The program uses the input provided to build the underlying (hyper)graph of a FSM (Petri net), and generates the (monoidal) free category on it using [idris-ct](https://github.com/statebox/idris-ct/). It then uses the initial state and path provided in the execution (call them `x` and `[x1, ... , xn]`, respectively) to evaluate the composition `idx;x1;...;xn`. It returns success or error depending if this defines a valid morphism in the (monoidal) free category or not.
66

77
The project uses [Typedefs](https://github.com/typedefs/typedefs) to encode types, which are serialized/deserialized in/from JSON.
88

@@ -19,12 +19,20 @@ This will install the binary in elba's binary folder. Typically `~/.elba/bin` if
1919
You can find elba and instructions on how to install it on the [official repository](https://github.com/elba/elba).
2020

2121
## Usage
22-
Just put your input (as specified below) in a file, for example `input.JSON`, and run:
22+
23+
To evaluate a Petri net, just put your input (as specified below) in a file, for example `input.JSON`, and run:
2324

2425
```
25-
fsm-oracle input.json
26+
fsm-oracle -p input.json
2627
```
2728

29+
If instead you want to evaluate a FSM, run:
30+
31+
```
32+
fsm-oracle --fsm input.json
33+
```
34+
35+
2836
If the execution is valid, Idris will return a json output of the following form:
2937

3038
```javascript
@@ -48,106 +56,262 @@ Where `x` denotes an error code according to the following table:
4856

4957
|Error Code|Description|
5058
|---|---|
51-
|`0`| The FSM specification is invalid. |
52-
|`1`| The FSM state is invalid. |
53-
|`2`| The FSM path is invalid. |
59+
|`0`| The specification is invalid. |
60+
|`1`| The initial state is invalid. |
61+
|`2`| The path is invalid. |
5462
|`3`|Input cannot be parsed as JSON. |
5563
|`4`|Filesystem error: File cannot be read. |
56-
## Input format
5764

58-
Input has to be fed as JSON, and is converted to Idris terms and types through the use of [Typedefs](https://github.com/typedefs/typedefs). The Idris types for FSM executions are defined in the file `Tgraph.idr`.
65+
## Input format
5966

60-
The internal input format is a term of type `FSMExec`, and is of the form
61-
`(FSMSpec, FSMState, FSMPath)`. It consists of three things: A specification of the FSM on which executions are run (`FSMSpec`), an initial state (`FSMState`), and a list of actions to evaluate (`FSMPath`).
67+
Input has to be fed as JSON, and is converted to Idris terms and types through the use of [Typedefs](https://github.com/typedefs/typedefs). The Idris types for Petri net executions are defined in the file `PetriFormat.idr`, while the ones for the FSM case are defined in `FSMFormat.idr`.
6268

63-
#### `FSMSpec`
64-
The type of `FSMSpec` is `(Nat,List (Nat Nat))`: The FSM is specified as a pair, where the first component denotes the number of states (vertexes) of the FSM, while the second is a list of pairs of vertexes (edgelist) denoting the possible actions.
6569

66-
For instance, `(5,[(2,1),(4,2),(0, 3)])` specifies a FSM having `5` vertexes, enumerated `0,1,2,3,4`, and three possible actions: One going from `2` to `1`, one going from `4` to `2` and one going from `0` to `3`.
67-
68-
The edgelist has to be in range as specified by the number of vertexes. As such, specifications such as `(5,[(7,1),(4,2),(0, 3)])`
69-
or `(5,[(5,5)])` are considered invalid and will produce an error.
70+
### Petri net execution format documentation
7071

71-
#### `FSMState`
72-
The type of `FSMState` is `Nat`. This specifies an initial vertex from which the computation has to start.
72+
Overall, an input as to be passed by giving the following JSON:
7373

74-
The initial state has to be in range as specified by the number of vertexes in `FSMSpec`. So, for instance, `4` is a valid state for the FSM `(5,[(2,1),(4,2),(0, 3)])`, while `5` is not, and will produce an error.
74+
```javascript
75+
{
76+
"_0": spec
77+
"_1": state
78+
"_2": path
79+
}
80+
```
81+
where `spec`, `state` and `path` are defined below.
7582

76-
#### `FSMPath`
77-
The type of `FSMPath` is `List Nat`. It specifies a computation to evaluate.
83+
This will be parsed into a term having type `PetriExec`. This is a record consisting of a three things: A term of type `PetriSpec k`, one of type `PetriState spec` and one of type
84+
`PetriPath (Places spec) k`.
7885

79-
Each number in the list has to be in range as specified by the length of the edgelist in `FSMSpec`. As such, `[1,0]` is a valid path for the FSM `(5,[(2,1),(4,2),(0, 3)])` (indicating to first use the action going from `4` to `2` and then the one going from `2` to `1`), while `[3]` is not.
86+
#### `spec`
87+
Internally, specifications have type of `PetriSpec k`, which is a type depending on a natural number `k`. It is a record consisting of `Places`, of type `Nat`, and `Edges`, of type `Vect k (List (Fin Places), List (Fin Places))`. `Places` enumerates the number of places in the net, while `Edges` consists of `k` pairs `(List (Fin Places), List (Fin Places))`. Each pair represents an edge, with the first component listing its input places, and the second component listing its output places.
8088

81-
#### Examples
82-
83-
The following define valid inputs:
89+
**A specification is passed to the oracle using JSON, and representing vertexes and edges as lists of pairs**. For instance, consider
90+
```javascript
91+
{
92+
"_0": 5,
93+
"_1": [
94+
{"_0": [0], "_1":[]},
95+
{"_0" : [1,1,1], "_1" : [0,2,3]},
96+
{"_0": [2,3,3], "_1" : [4]},
97+
{"_0": [1], "_1" : [4,3]},
98+
{"_0": [4,4,4], "_1": [4]},
99+
{"_0": [], "_1" : [4,4]}
100+
]
101+
}
84102
```
85-
((5, [(1,1),(3,4),(2,1)]) , 3, [1])
86-
((5, [(1,1),(1,1),(2,1)]) , 2, [2,1,0])
103+
This piece of JSON defines what has to be put in place of `spec` in
104+
```javascript
105+
{
106+
"_0": spec
107+
"_1": state
108+
"_2": path
109+
}
87110
```
111+
It specifies the Petri net of type `PetriSpec 6`, having:
112+
- `5` vertexes, enumerated `0,1,2,3,4`
113+
- `6` transitions: One going from `0` to nothing (no outputs), one going from `1,1,1` to `0,2,3`, and so on.
114+
You can denote transitions that produce more than
115+
one token in the same place by just repeating the token itself,
116+
as in `{"_0": [2,3,3], "_1" : [4]}` in the example above.
117+
Similarly, an empty list signifies empty inputs or outputs.
118+
119+
Notice that the `k` parameter in `PetriSpec k` is automatically
120+
inferred at runtime by parsing the length of the edgelist.
121+
For instance, in the example above the inferred parameter is `6`, since the list
88122

89-
The following define invalid inputs:
123+
```javascript
124+
[
125+
{"_0": [0], "_1":[]},
126+
{"_0" : [1,1,1], "_1" : [0,2,3]},
127+
{"_0": [2,3,3], "_1" : [4]},
128+
{"_0": [1], "_1" : [4,3]},
129+
{"_0": [4,4,4], "_1": [4]},
130+
{"_0": [], "_1" : [4,4]}
131+
]
132+
```
133+
has `6` entries.
90134

91-
Invalid `FSMSpec`:
92-
`((5, [(1,1),(5,4),(2,1)]) , 2, [2,0,1])`
135+
The edgelist given at runtime has to be in range as specified by the number of vertexes. Failing to do so produces a type mismatch. As such, a specification such as
93136

94-
Invalid `FSMState`:
95-
`((5, [(1,1),(3,4),(2,1)]) , 6, [2,1,0])`
137+
```javascript
138+
{
139+
"_0": 5,
140+
"_1": [
141+
{"_0": [5], "_1":[]}
142+
]
143+
}
144+
```
145+
is invalid (input of the first transition is not in range), and will produce an error.
96146

97-
Invalid `FSMPath`:
98-
`((3,[]), 1, [1])`
147+
#### `state`
148+
Internally, a starting state has type `PetriState spec`, that is defined to be `List (Fin (Places spec))`, with `spec` having type `PetriSpec k` for some `k`. This specifies an initial list of places from which the computation has to start. For instance, `[3,4,4,1]` means "a token in `3`, two in `4`, one in `1`".
99149

100-
#### JSON Encoding
150+
**In json, this is just specified using list notation.** For instance, `[3,4,4,1]` can be put in place of `state` in
151+
```javascript
152+
{
153+
"_0": spec
154+
"_1": state
155+
"_2": path
156+
}
157+
```
158+
159+
Again, the initial state specified in the input has to be in range as specified by the number of vertexes in `PetriSpec`. So, for instance, `[4,2,0]` is a valid state for the spec example in the previous section, while `[5]` is not, and will produce an error.
101160

102-
Terms of type `FSMSpec` as described above have to be fed as inputs, encoded in JSON format. The way JSON encoding is implemented can be found in the file `JSONFormat.idr`.
161+
#### `path`
162+
Internally, a path has type `PetriPath places k`. This is used to define a type `Tree (Fin places) (Fin k)`, where `places` and `k` represent the number of places and transitions given in a specification. A path consists in a tree indexed by two natural numbers `o` and `m`
163+
```
164+
data Tree o m = Tensor (Tree o m) (Tree o m)
165+
| Sequence (Tree o m) (Tree o m)
166+
| Sym o o
167+
| Id o
168+
| Mor m
169+
```
103170

104-
We do use the notation:
171+
#### Examples
105172

173+
The following defines a valid input:
106174
```javascript
107175
{
108-
"_1":
109-
"_2":
110-
...
111-
"_n":
176+
"_0": {
177+
"_0": 5,
178+
"_1": [
179+
{"_0": [0], "_1":[]},
180+
{"_0" : [1,1,1], "_1" : [0,2,3]},
181+
{"_0": [2,3,3], "_1" : [4]},
182+
{"_0": [1], "_1" : [4,3]},
183+
{"_0": [4,4,4], "_1": [4]},
184+
{"_0": [], "_1" : [4,4]}
185+
]
186+
},
187+
"_1": [0],
188+
"_2": {
189+
"inn": {
190+
"_3": 0
191+
}
192+
}
112193
}
113194
```
114-
To encode tuples, and the usual square bracket notation for lists. Pairs defining edges are encoded as:
195+
196+
Instead, the following defines an invalid input:
115197
```javascript
116198
{
117-
"input":
118-
"output":
199+
"_0": {
200+
"_0": 1,
201+
"_1": []
202+
},
203+
"_1": [],
204+
"_2": {
205+
"inn": {
206+
"_1": {
207+
"_1": {
208+
"_1": {
209+
"_0": 0
210+
}
211+
}
212+
}
213+
}
214+
}
119215
}
120216
```
121-
Where `input` and `output` specify the endpoints of the edge.
122217

123-
Applying these definitions recursively, any term of type `FSMExec` can be encoded. For example, the following is the JSON encoding of the input execution `((5, [(1,1),(3,4),(2,1)]) , 2, [2,0,0])`:
218+
### FSM net execution format documentation
124219

220+
For FSMs, the internal input format is a term of type `FSMExec`, and is of the form
221+
`(FSMSpec, FSMState, FSMPath)`. It consists of three things: A specification of the FSM on which executions are run (`FSMSpec`), an initial state (`FSMState`), and a list of actions to evaluate (`FSMPath`).
125222

223+
This is fed exactly as we do for Petri nets, using the JSON:
126224
```javascript
127225
{
128-
"_0": {
226+
"_0": spec
227+
"_1": state
228+
"_2": path
229+
}
230+
```
231+
232+
For FSMs, though, the definition of `spec`, `state` and `path` are different, and given below:
233+
234+
#### `spec`
235+
The type of `FSMSpec` is `(Nat,List (Nat Nat))`: The FSM is specified as a pair, where the first component denotes the number of states (vertexes) of the FSM, while the second is a list of pairs of vertexes (edgelist) denoting the possible actions.
236+
237+
For instance, `(5,[(2,1),(4,2),(0, 3)])` specifies a FSM having `5` vertexes, enumerated `0,1,2,3,4`, and three possible actions: One going from `2` to `1`, one going from `4` to `2` and one going from `0` to `3`.
238+
239+
**A specification is passed to the oracle using JSON, and representing vertexes and edges as lists of pairs**. For instance, consider
240+
```javascript
129241
"_0": 5,
130242
"_1": [
131243
{
132-
"input": 1,
244+
"input": 2,
133245
"output": 1
134246
},
135247
{
136-
"input": 3,
137-
"output": 4
248+
"input": 4,
249+
"output": 2
138250
},
139251
{
140-
"input": 2,
141-
"output": 1
252+
"input": 0,
253+
"output": 3
142254
}]
143-
},
144-
"_1": 2,
145-
"_2": [2, 0, 0]
255+
```
256+
This piece of JSON defines what has to be put in place of `spec` in
257+
```javascript
258+
{
259+
"_0": spec
260+
"_1": state
261+
"_2": path
262+
}
263+
```
264+
265+
The edgelist has to be in range as specified by the number of vertexes. As such, specifications such as `(5,[(7,1),(4,2),(0, 3)])`
266+
or `(5,[(5,5)])` are considered invalid and will produce an error.
267+
268+
269+
#### `state`
270+
The type of `FSMState` is `Nat`. This specifies an initial vertex from which the computation has to start. In the JSON input we represent it just as it is.
271+
Hence, any natural number can be put in place of `state` in the JSON:
272+
```javascript
273+
{
274+
"_0": spec
275+
"_1": state
276+
"_2": path
277+
}
278+
```
279+
The initial state has to be in range as specified by the number of vertexes in `FSMSpec`. So, for instance, `4` is a valid state for the FSM `(5,[(2,1),(4,2),(0, 3)])`, while `5` is not, and will produce an error.
280+
281+
#### `path`
282+
The type of `FSMPath` is `List Nat`. It specifies a computation to evaluate.
283+
284+
In JSON we represent it just as a list. As such, any list of natural numbers can be put in place of `path` in the JSON:
285+
```javascript
286+
{
287+
"_0": spec
288+
"_1": state
289+
"_2": path
146290
}
147-
```
291+
```
292+
Each number in the list has to be in range as specified by the length of the edgelist in `FSMSpec`. As such, `[1,0]` is a valid path for the FSM `(5,[(2,1),(4,2),(0, 3)])` (indicating to first use the action going from `4` to `2` and then the one going from `2` to `1`), while `[3]` is not.
293+
294+
#### Examples
295+
296+
The following define valid inputs:
297+
```
298+
((5, [(1,1),(3,4),(2,1)]) , 3, [1])
299+
((5, [(1,1),(1,1),(2,1)]) , 2, [2,1,0])
300+
```
301+
302+
The following define invalid inputs:
303+
304+
Invalid `FSMSpec`:
305+
`((5, [(1,1),(5,4),(2,1)]) , 2, [2,0,1])`
306+
307+
Invalid `FSMState`:
308+
`((5, [(1,1),(3,4),(2,1)]) , 6, [2,1,0])`
309+
310+
Invalid `FSMPath`:
311+
`((3,[]), 1, [1])`
148312

149313
### License
150314

151315
Unless explicitly stated otherwise all files in this repository are licensed under the GNU Affero General Public License.
152316

153-
Copyright © 2020 [Stichting Statebox](https://statebox.nl).
317+
Copyright © 2020 [Stichting Statebox](https://statebox.nl).

‎elba.lock‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
[[packages]]
2-
id = 'fsm-oracle/fsm-oracle@dir+/Users/zephyz/Statebox/idris-fsm-oracle'
2+
id = 'fsm-oracle/fsm-oracle@dir+/Users/av82/statebox/fsm-oracle'
33
version = '0.1.0'
44

55
[[packages.dependencies]]
@@ -65,3 +65,4 @@ dependencies = []
6565
id = 'japesinator/Idris-Bifunctors@git+https://github.com/andrevidela/Idris-Bifunctors#f8dfb7f89d321afccf2086cb04c64f45a63d3712'
6666
version = '0.1.0'
6767
dependencies = []
68+
es = []

‎elba.toml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,4 +11,4 @@ authors = []
1111
path = "src"
1212
name = "fsm-oracle"
1313
main = "Main"
14-
idris_opts = ["-p", "contrib", "-p", "idris-ct"]
14+
idris_opts = ["-p", "contrib"]

‎petriTestExec.json‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
{
2+
"_0": {
3+
"_0": 5,
4+
"_1": [{"_0": [0], "_1":[]},
5+
{"_0" : [1,1,1], "_1" : [0,2,3]},
6+
{"_0": [2,3,3], "_1" : [4]},
7+
{"_0": [1], "_1" : [4,3]},
8+
{"_0": [4,4,4], "_1": [4]},
9+
{"_0": [], "_1" : [4,4]}]},
10+
"_1": [0],
11+
"_2": {
12+
"inn": {
13+
"_3": 0
14+
}
15+
}
16+
}

0 commit comments

Comments
 (0)