内容简介:A formally verified idris program that evaluates executions for finite state machines (FSM).The program uses the input provided inThe project uses
Statebox's FSM-Oracle
A formally verified idris program that evaluates executions for finite state machines (FSM).
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
. 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.
The project uses Typedefs to encode types, which are serialized/deserialized in/from JSON.
Installation
We use elba
to download dependencies and compile the binary, just type:
$ elba install
This will install the binary in elba's binary folder. Typically ~/.elba/bin
if this folder is in your path you can simply call fsm-oracle
to test it out.
You can find elba and instructions on how to install it on the official repository .
Usage
Just put your input (as specified below) in a file, for example input.JSON
, and run:
fsm-oracle input.json
If the execution is valid, Idris will return a json output of the following form:
{ "_0": {} }
If the execution produces an error, the output will be:
{ "_1": { "inn" : { "_x": {} } } }
Where x
denotes an error code according to the following table:
Error Code | Description |
---|---|
0
|
The FSM specification is invalid. |
1
|
The FSM state is invalid. |
2
|
The FSM path is invalid. |
3
|
Input cannot be parsed as JSON. |
4
|
Filesystem error: File cannot be read. |
Input format
Input has to be fed as JSON, and is converted to Idris terms and types through the use of Typedefs
. The Idris types for FSM executions are defined in the file Tgraph.idr
.
The internal input format is a term of type FSMExec
, and is of the form (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
).
FSMSpec
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.
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
.
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)])
or (5,[(5,5)])
are considered invalid and will produce an error.
FSMState
The type of FSMState
is Nat
. This specifies an initial vertex from which the computation has to start.
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.
FSMPath
The type of FSMPath
is List Nat
. It specifies a computation to evaluate.
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.
Examples
The following define valid inputs:
((5, [(1,1),(3,4),(2,1)]) , 3, [1]) ((5, [(1,1),(1,1),(2,1)]) , 2, [2,1,0])
The following define invalid inputs:
Invalid FSMSpec
: ((5, [(1,1),(5,4),(2,1)]) , 2, [2,0,1])
Invalid FSMState
: ((5, [(1,1),(3,4),(2,1)]) , 6, [2,1,0])
Invalid FSMPath
: ((3,[]), 1, [1])
JSON Encoding
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
.
We do use the notation:
{ "_1": "_2": ... "_n": }
To encode tuples, and the usual square bracket notation for lists. Pairs defining edges are encoded as:
{ "input": "output": }
Where input
and output
specify the endpoints of the edge.
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])
:
{ "_0": { "_0": 5, "_1": [ { "input": 1, "output": 1 }, { "input": 3, "output": 4 }, { "input": 2, "output": 1 }] }, "_1": 2, "_2": [2, 0, 0] }
License
Unless explicitly stated otherwise all files in this repository are licensed under the GNU Affero General Public License.
Copyright © 2020 Stichting Statebox .
以上就是本文的全部内容,希望本文的内容对大家的学习或者工作能带来一定的帮助,也希望大家多多支持 码农网
猜你喜欢:本站部分资源来源于网络,本站转载出于传递更多信息之目的,版权归原作者或者来源机构所有,如转载稿涉及版权问题,请联系我们。
Nine Algorithms That Changed the Future
John MacCormick / Princeton University Press / 2011-12-27 / GBP 19.95
Every day, we use our computers to perform remarkable feats. A simple web search picks out a handful of relevant needles from the world's biggest haystack: the billions of pages on the World Wide Web.......一起来看看 《Nine Algorithms That Changed the Future》 这本书的介绍吧!