Stochastic Timed Reo Modeling |
This is a compositional modeling framework for **Stochastic Timed Reo** in Python (pyConnectors). All the sources can be found here.
All primitive channels are defined in 'channels.py'. The semantics of primitive channels are specified correspondingly in 'semantics/STAr/channel.py'. The 'Connector' class (defined in 'connector.py') enables users to construct complex connectors based on the primitive channels and other sub-connectors in a compositional manner. Semantics of the connectors can be obtained automatically.
Python 3 is required. No more dependencies are needed.
Generally, it has the following features:
Users can create new types of channels according to your scenarios (tasks) by specifying the 'ports' and supported 'parameters'. Here shows an exmaple of the specification of 'Sync' channel and its semantics as 'STAr'.
```
Sync = Connector("Sync")
Sync.createPort(PORT_IO_IN, 'A')
Sync.createPort(PORT_IO_OUT, 'B')
Sync.setTypeChannel()
```
```
s = STA()
A = s.createAction("A")
B = s.createAction("B")
l0 = s.createLocation("l0")
s.setInitialLocation(l0)
s.createTransition()\
.startFrom(l0)\
.endAt(l0)\
.setActions([A, B])\
.setGuard(Value(True))\
.addAssignment(s.getVariableByAction(B), s.getVariableByAction(A))
```
Complex connectors are constructed through the set of primitive channels (and other sub-connectors) and the connections. The corresponding semantics can be obtained through the 'getSemantics' function without manual specification.
```
doubleSync = Connector("double sync")
A = doubleSync.createPort(PORT_IO_IN, 'A')
B = doubleSync.createPort(PORT_IO_OUT, 'B')
M = doubleSync.createNode()
Sync.connect(A, M)
Sync.connect(M, B)
```
The specification of PTCTLr is supported in the framework. The framework also supports the translation from the specification of connectors and the properties into PRISM model and the corresponding property specification.
A property formalizing the synchoronization of the actions on the input and output ports for 'doubleSync' is shown as follows.
```
doubleSync.addProperty(
"Sync",
Property.G(Expr.derive(PortTriggered(A), PortTriggered(B)))
)
```
Here we present an example demonstrating the construction of connectors based on the primitive channels, along with the follow-up translation to PRISM specification.
A probabilistic router is with one input port and two output ports, which are specified through the 'createPort' method. Intermediate nodes are constructed through the 'createNodes' method. The probabilistic router is comprised of five types of channels including *Sync*, *SyncDrain*, *LossySync*, *StochasticChoice*, *Filter*.
It would dispatch the input data items to the sink ends in a probabilistic manner where the probability for the data transfer is parameterized.
The specification is as follows:
```
PRouter = Connector("Probabilistic Router")
A = PRouter.createPort(PORT_IO_IN, 'A')
E, F = PRouter.createPorts(PORT_IO_OUT, 'E', 'F')
M, C, B, D, A1, B1 = PRouter.createNodes(6)
v = Variable(name='x')
Sync.connect(A, M)
SyncDrain.connect(M, C)
LossySync.connect(M, B)
LossySync.connect(M, D)
Sync.connect(B, C)
Sync.connect(D, C)
Sync.connect(B, E)
Sync.connect(D, F)
StochasticChoice.connect(M, A1, params={'dist': BinaryDistribution(0.2)})
Filter.connect(A1, B1, params={'f': (v, EqExpr(v, 1))})
SyncDrain.connect(B1, B)
```
The property we intend to verify is the data items would be sent to the sink ends with probability 1. Here is the specification.
```
PRouter.addProperty(
"message will not get lost",
Property.geq(
Property.Pmin(
Property.G(Expr.derive(PortTriggered(A), Expr.lor(PortTriggered(E), PortTriggered(F))))
),
Value(1)
)
)
```
PRISM model and property specification could be obtained through the core functions 'getSemantics' and 'sta2prism'. Users can save the translated models and properties into a target file (specified by users) through function 'gen_file'. Here shows the translated model and property specification of the probabilistic router.
```
pta
module main
d_PA_IN : int init 0;
st_PA_IN : bool init false;
d_PE_OUT : int init 0;
st_PE_OUT : bool init false;
d_PF_OUT : int init 0;
st_PF_OUT : bool init false;
sample_0 : int;
loc: [0..2] init 0;
invariant
(true)
endinvariant
[act_PA_IN_PE_OUT] ((sample_0 = 1)) & (loc = 1) ->
1.000000 : (loc' = 0) & (st_PA_IN' = true) & (st_PE_OUT' = true) & (st_PF_OUT' = false) & (d_PE_OUT' = d_PA_IN);
[act_PA_IN_PF_OUT] ((!(sample_0 = 1))) & (loc = 1) ->
1.000000 : (loc' = 0) & (st_PA_IN' = true) & (st_PE_OUT' = false) & (st_PF_OUT' = true) & (d_PF_OUT' = d_PA_IN);
[act_] (true) & (loc = 0) ->
0.200000 : (loc' = 1) & (st_PA_IN' = false) & (st_PE_OUT' = false) & (st_PF_OUT' = false) & (sample_0' = 0) +
0.800000 : (loc' = 1) & (st_PA_IN' = false) & (st_PE_OUT' = false) & (st_PF_OUT' = false) & (sample_0' = 1);
[act_] (true) & (loc = 0) ->
1.000000 : (loc' = 0) & (st_PA_IN' = false) & (st_PE_OUT' = false) & (st_PF_OUT' = false);
[act_] (true) & (loc = 1) ->
1.000000 : (loc' = 1) & (st_PA_IN' = false) & (st_PE_OUT' = false) & (st_PF_OUT' = false);
endmodule
// PROPERTY message will not get lost
(1 <= Pmin=? [ G (((!(st_PA_IN)) | ((st_PE_OUT) | (st_PF_OUT)))) ])
```