Skip to content

Commit 8a922a8

Browse files
author
Matt Luckcuck
committed
Merge branch 'ltl2cspStatemachine'
2 parents 23afe17 + dea5ba3 commit 8a922a8

File tree

11 files changed

+441
-89
lines changed

11 files changed

+441
-89
lines changed

‎README.md

Lines changed: 15 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
# Varanus 0.9.3
1+
# Varanus 0.9.4
22
### Matt Luckcuck
33
### Runtime Verification Toolchain using CSP and FDR
44

@@ -52,31 +52,26 @@ Varanus is a terminal program within the `varanus/varanus-python` directory.
5252
The basic usage is to run `varanus.py` passing a parameter that indicates either `online` or `offline` Runtime Verification, and a parameter that is the filepath of a `config` file (which, in turn, will point Varanus at the CSP model and System Under Analysis).
5353

5454
The basic workflow is:
55-
\* Write a CSP specification for the System Under Analysis
56-
\* Build the config file to point Varanus at the System Under Analysis and the CSP specification (and some other parameters)
57-
\* Run Varanus on the config file, telling it if it should do online or offline RV (if it's offline then the 'system' it is monitoring will be a trace file, also written separately.)
55+
* Write a CSP specification for the System Under Analysis
56+
* Build the config file to point Varanus at the System Under Analysis and the CSP specification (and some other parameters)
57+
* Run Varanus on the config file, telling it if it should do online or offline RV (if it's offline then the 'system' it is monitoring will be a trace file, also written separately.)
5858

5959
```bash
60-
usage: varanus.py [-h] [--model MODEL] [--map MAP] [-n NAME]
61-
[--log_path LOG_PATH] [-t TRACE_FILE] [-s SPEED]
62-
{offline,online,sm-test,offline-test} config
60+
usage: varanus.py [-h] [-n NAME] [-l LOG_PATH]
61+
{offline,online,sm-test,offline-test,stress-test,build-only}
62+
config
6363

6464
positional arguments:
65-
{offline,online,sm-test,offline-test}
66-
The type of check to be performed
67-
config The location of the config file
65+
{offline,online,sm-test,offline-test,stress-test,build-only}
66+
The type of action or check for Varanus to perform.
67+
config The location of the config file.
6868

6969
optional arguments:
7070
-h, --help show this help message and exit
71-
--model MODEL The location of the model used as the oracle.
72-
--map MAP The location of the event map
73-
-n NAME, --name NAME The name of the check and therefore name of the log
74-
file
75-
--log_path LOG_PATH The path of the log dir
76-
-t TRACE_FILE, --trace_file TRACE_FILE
77-
The location of the trace file. Only used if
78-
type='offline'
79-
-s SPEED, --speed SPEED Run 10 timed run and produce the times and mean.).
71+
-n NAME, --name NAME Override the config file's name. This is the name of
72+
the check and therefore name of the log file.
73+
-l LOG_PATH, --log_path LOG_PATH
74+
Override the default log path.
8075
```
8176
8277
Since Varanus 0.9.0 the parameters can be set in the config file, and some can be overridden at the command line.
@@ -107,7 +102,7 @@ The config file sets the following parameters:
107102
108103
### Quick Check
109104
110-
As a quick check that Varanus is installed correctly, you can enter the `varanus` root directly and run `python varanus-python/varanus.py offline-test rosmon-test/hibye.yaml` (assuming your `python` command points to Python 2.x) to run a very simple check on a simple process. If all is well, you should see `INFO:varanus:Trace file finished with no violations` at the end of the output to the terminal.
105+
As a quick check that Varanus is installed correctly, you can enter the `varanus` root directly and run `python varanus-python/varanus.py offline rosmon-test/hibye.yaml` (assuming your `python` command points to Python 2.x) to run a very simple check on a simple process. If all is well, you should see `INFO:varanus:Trace file finished with no violations` at the end of the output to the terminal.
111106
112107
Lets look at the config file we've just checked:
113108

‎tools/README.md

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
# Varanus Tools
2+
3+
A collection of tools to support Varanus and CSP verification.
4+
5+
## `csp2dot`
6+
7+
This tool converts a CSPStateMachine object to a DOT object or string, to enable simple visulaisation.
8+
9+
### Installation
10+
11+
`csp2dot` relies on `pydot`, which can be installed using
12+
```bash
13+
pip install pydot
14+
```
15+
16+
### Usage
17+
18+
TBD

‎tools/csp2dot.py

Lines changed: 72 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,72 @@
1+
import pydot
2+
import sys
3+
import os
4+
sys.path.insert(0, os.path.abspath('../varanus-python'))
5+
from csp_state_machine import *
6+
7+
def state_machine_2_dot(csp_machine):
8+
graph = pydot.Dot("CSP Process", graph_type="digraph", bgcolor="grey")
9+
for state in csp_machine.states.values():
10+
graph.add_node(pydot.Node(state.name, shape="circle"))
11+
12+
for transition in state.transitions.values():
13+
14+
t_name = transition.name
15+
if t_name == Transition._TERMINATE:
16+
t_name = "Tick"
17+
graph.add_edge(pydot.Edge(state.name, transition.get_destination().name, label=t_name))
18+
19+
graph.write_png("csp_graph.png")
20+
21+
22+
def state_machine_2_dot_string(csp_machine):
23+
24+
dot_string = "digraph CSPProcess{\nbgcolor = grey\n"
25+
26+
for state in csp_machine.states.values():
27+
#graph.add_node(pydot.Node(state.name, shape="circle"))
28+
dot_string += str(state.name) + "[shape=circle]\n"
29+
30+
for transition in state.transitions.values():
31+
32+
t_name = transition.name
33+
if t_name == Transition._TERMINATE:
34+
t_name = "Tick"
35+
#graph.add_edge(pydot.Edge(state.name, transition.get_destination().name, label=t_name))
36+
dot_string += str(state.name) + " -> " + str(transition.get_destination().name) + " [label="+str(t_name)+"]\n"
37+
dot_string += "}"
38+
graphs = pydot.graph_from_dot_data(dot_string)
39+
graphs[0].write_png("csp_graph.png")
40+
41+
42+
43+
if __name__ == "__main__":
44+
""" Test the CSP State Machine"""
45+
46+
machine = CSPStateMachine()
47+
48+
csp_dict = {0: [("a",1)],1: [("b",2)], 2: [(Transition._TERMINATE, 3)], 3: [] }
49+
machine.load_from_dictionary(csp_dict)
50+
machine.start()
51+
print(str(machine.to_dictionary()))
52+
#state_machine_2_dot(machine)
53+
#state_machine_2_dot_string(machine)
54+
55+
dot_string = machine.to_DOT()
56+
graphs = pydot.graph_from_dot_data(dot_string)
57+
graphs[0].write_png("csp_graph.png")
58+
59+
machine2 = CSPStateMachine()
60+
61+
csp_dict = {0: [("a",1), ("c", 2)],1: [("b",0), ("c", 2)], 2: [(Transition._TERMINATE, 3)], 3: [] }
62+
machine.load_from_dictionary(csp_dict)
63+
machine.start()
64+
print(str(machine.to_dictionary()))
65+
#state_machine_2_dot(machine)
66+
#state_machine_2_dot_string(machine)
67+
68+
dot_string = machine.to_DOT()
69+
graphs = pydot.graph_from_dot_data(dot_string)
70+
graphs[0].write_png("csp_graph2.png")
71+
72+
print("Done")

‎tools/ltl_translator.py

Lines changed: 146 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,146 @@
1+
import sys
2+
import string
3+
import spot
4+
import buddy
5+
import os
6+
sys.path.insert(0, os.path.abspath('../varanus-python'))
7+
from csp_state_machine import *
8+
9+
def ltl2cspstatemachine(ltl):
10+
machine = CSPStateMachine()
11+
csp = 'channel '
12+
monitor = spot.translate(ltl, 'monitor', 'det', 'complete')
13+
l = []
14+
for ap in monitor.ap():
15+
l.append(f'{ap}')
16+
print(ap)
17+
machine.add_letter_to_alphabet(ap)
18+
csp += ', '.join(l) + '\n\n'
19+
transitions = {}
20+
for s in range(0, monitor.num_states()):
21+
transitions[str(s)] = {}
22+
for t in monitor.out(s):
23+
for ap in monitor.ap():
24+
ap = str(ap)
25+
bdd = buddy.bddtrue
26+
for ap1 in monitor.ap():
27+
ap1 = str(ap1)
28+
if ap == ap1:
29+
p = monitor.register_ap(ap1)
30+
bdd = bdd & buddy.bdd_ithvar(p)
31+
else:
32+
p = monitor.register_ap(ap1)
33+
bdd = bdd & buddy.bdd_nithvar(p)
34+
if (t.cond & bdd) != buddy.bddfalse:
35+
transitions[str(s)][ap] = str(t.dst)
36+
print(str(transitions))
37+
for s in transitions:
38+
csp += f'state{s} = \n'
39+
print(s)
40+
machine.add_destination(s)
41+
l = []
42+
for ap in transitions[s]:
43+
l.append(f'{ap} -> state{transitions[s][ap]}')
44+
machine.add_transition_by_name(ap, s, transitions[s][ap])
45+
csp += '\n[]\n'.join(l)
46+
csp += '\n\n'
47+
csp += f'WCST = state{monitor.get_init_state_number()} -- Main Process, starts the recursion in state{monitor.get_init_state_number()}\n\n'
48+
csp += f'assert state{monitor.get_init_state_number()}; RUN(Events) :[deadlock free]:\n'
49+
csp += f'assert state{monitor.get_init_state_number()} :[deterministic]:\n'
50+
csp += f'assert state{monitor.get_init_state_number()} :[divergence free]:'
51+
return machine
52+
53+
def ltl2csp(ltl):
54+
csp = 'channel '
55+
monitor = spot.translate(ltl, 'monitor', 'det', 'complete')
56+
l = []
57+
for ap in monitor.ap():
58+
l.append(f'{ap}')
59+
csp += ', '.join(l) + '\n\n'
60+
transitions = {}
61+
for s in range(0, monitor.num_states()):
62+
transitions[str(s)] = {}
63+
for t in monitor.out(s):
64+
for ap in monitor.ap():
65+
ap = str(ap)
66+
bdd = buddy.bddtrue
67+
for ap1 in monitor.ap():
68+
ap1 = str(ap1)
69+
if ap == ap1:
70+
p = monitor.register_ap(ap1)
71+
bdd = bdd & buddy.bdd_ithvar(p)
72+
else:
73+
p = monitor.register_ap(ap1)
74+
bdd = bdd & buddy.bdd_nithvar(p)
75+
if (t.cond & bdd) != buddy.bddfalse:
76+
transitions[str(s)][ap] = str(t.dst)
77+
print(str(transitions))
78+
for s in transitions:
79+
csp += f'state{s} = \n'
80+
l = []
81+
for ap in transitions[s]:
82+
l.append(f'{ap} -> state{transitions[s][ap]}')
83+
csp += '\n[]\n'.join(l)
84+
csp += '\n\n'
85+
csp += f'WCST = state{monitor.get_init_state_number()} -- Main Process, starts the recursion in state{monitor.get_init_state_number()}\n\n'
86+
csp += f'assert state{monitor.get_init_state_number()}; RUN(Events) :[deadlock free]:\n'
87+
csp += f'assert state{monitor.get_init_state_number()} :[deterministic]:\n'
88+
csp += f'assert state{monitor.get_init_state_number()} :[divergence free]:'
89+
return csp
90+
91+
def ltl2rml(ltl):
92+
rml = ''
93+
monitor = spot.translate(ltl, 'monitor', 'det', 'complete')
94+
l = []
95+
for ap in monitor.ap():
96+
l.append(f'{ap} matches {{ event: \'{ap}\' }};')
97+
rml += '\n'.join(l) + '\n\n'
98+
transitions = {}
99+
for s in range(0, monitor.num_states()):
100+
transitions[str(s)] = {}
101+
for t in monitor.out(s):
102+
for ap in monitor.ap():
103+
ap = str(ap)
104+
bdd = buddy.bddtrue
105+
for ap1 in monitor.ap():
106+
ap1 = str(ap1)
107+
if ap == ap1:
108+
p = monitor.register_ap(ap1)
109+
bdd = bdd & buddy.bdd_ithvar(p)
110+
else:
111+
p = monitor.register_ap(ap1)
112+
bdd = bdd & buddy.bdd_nithvar(p)
113+
if (t.cond & bdd) != buddy.bddfalse:
114+
transitions[str(s)][ap] = str(t.dst)
115+
print(str(transitions))
116+
for s in transitions:
117+
if s == str(monitor.get_init_state_number()):
118+
rml += 'Main = '
119+
else:
120+
rml += f'state{s} = '
121+
l = []
122+
for ap in transitions[s]:
123+
if str(monitor.get_init_state_number()) == transitions[s][ap]:
124+
l.append(f'{ap} Main')
125+
else:
126+
l.append(f'{ap} state{transitions[s][ap]}')
127+
128+
rml += ' \/ '.join(l)
129+
rml += ';\n'
130+
return rml
131+
132+
def main(args):
133+
ltl = args[1]
134+
#with open('../evaluation/monitor.csp', 'w') as file:
135+
# file.write(ltl2csp(ltl))
136+
# with open('../evaluation/monitor.rml', 'w') as file:
137+
# file.write(ltl2rml(ltl))
138+
machine = ltl2cspstatemachine(ltl)
139+
print(str(machine))
140+
141+
for s in machine.destinations.values():
142+
for trans in s.transitions:
143+
print(trans)
144+
145+
if __name__ == '__main__':
146+
main(sys.argv)

‎varanus-python/csp_lts.py

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
2+
_TERMINATE = '\xe2\x9c\x93'
3+
"""this is FDR's terminate transition, tick; if we see this we just go to the next state"""
4+
5+
_TAU = '\xcf\x84'
6+
"""The tau character."""
7+
class CSPLTS(object):
8+
9+
def __init__(self, name = None, states = None):
10+
if name is None:
11+
self.name = "CSP LTS"
12+
else:
13+
self.name = name
14+
15+
if states is None:
16+
self.states = {}
17+
else:
18+
self.states = states
19+
20+
def add_state(self, name):
21+
new_state = State(name)
22+
self.states[name] = new_state
23+
24+
25+
class State(object):
26+
27+
def __init__(self, name, transitions = None):
28+
self.name = name
29+
30+
if transitions is None:
31+
transitions = {}
32+
33+

0 commit comments

Comments
 (0)