-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathstructs.py
More file actions
85 lines (71 loc) · 2.72 KB
/
structs.py
File metadata and controls
85 lines (71 loc) · 2.72 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
from enum import Enum
class Automaton:
"""
An automaton has three types of states: `acc`, `dead`, normal.
For a run to be accepted, it should satisfy:
G(!dead) & GF(acc)
Thus, in the automaton `dead` states has the property that they are `trap` states.
If there are no `acc` states, acc is set to True.
If there are no `dead` states, dead is set to False.
"""
def __init__(self,
states,
init_state,
acc_states,
dead_states,
is_safety, # `safety` means an automaton encodes rejecting finite traces
edges: 'tuple of ((src,dst),set of labels) where label is a tuple of literals'):
self.states = states
self.init_state = init_state
self.acc_states = acc_states
self.dead_states = dead_states
self.edges = edges
self.propositions = self._get_propositions()
self.is_safety = is_safety
assert self.acc_states
assert not (self.is_safety and len(self.dead_states) == 0), str(self)
def _get_propositions(self):
propositions = set()
for ((src, dst), labels) in self.edges:
for label in labels:
for lit in label:
atom = lit.strip('~').strip('!')
propositions.add(atom)
return tuple(propositions) # fixing the order
def __str__(self):
return 'states: %s, init_state: %s, acc_states: %s, dead_states: %s, edges: %s' % \
(self.states, self.init_state, self.acc_states, self.dead_states, self.edges)
class SmvModule:
def __init__(self, name, module_inputs, desc, module_str, has_bad, has_fair):
self.module_inputs = tuple(module_inputs)
self.name = name
self.desc = desc
self.module_str = module_str
self.has_bad = has_bad
self.has_fair = has_fair
def __str__(self):
return 'module: %s (%s), def:\n%s' % (self.name, self.desc, self.module_str)
class SpecType(Enum):
AUTOMATON_SPEC = 1
LTL_SPEC = 2
PLTL_SPEC = 3
ORE_SPEC = 4
class PropertySpec:
def __init__(self,
desc,
is_positive: bool or None,
is_guarantee: bool or None,
data,
type: SpecType):
self.desc = desc
self.is_positive = is_positive
self.is_guarantee = is_guarantee
self.data = data
self.type = type
def __str__(self):
return "Spec(desc=%s, data=%s, %s, %s)" % \
(self.desc,
self.data,
['assumption', 'guarantee'][self.is_guarantee],
['bad trace', 'good trace'][self.is_positive])
__repr__ = __str__