Skip to content

Commit 23afe17

Browse files
author
Matt Luckcuck
committed
2 parents 2a37415 + 3c14949 commit 23afe17

File tree

1 file changed

+149
-0
lines changed

1 file changed

+149
-0
lines changed

‎tools/ltl2csp_rml.py

Lines changed: 149 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,149 @@
1+
import sys
2+
import argparse
3+
import spot
4+
import buddy
5+
6+
# Function to convert an LTL formula into a CSP model
7+
def ltl2csp(ltl):
8+
csp = 'channel ' # Start the CSP model with the 'channel' declaration
9+
# Translate the LTL formula to a monitor automaton using Spot
10+
monitor = spot.translate(ltl, 'monitor', 'det', 'complete')
11+
print(monitor.to_str())
12+
l = [] # Initialize a list to hold atomic propositions (APs)
13+
14+
# Collect all atomic propositions (APs) used in the monitor
15+
for ap in monitor.ap():
16+
l.append(f'{ap}')
17+
18+
# Add APs to the CSP channel declaration
19+
csp += ', '.join(l) + '\n\n'
20+
21+
transitions = {} # Dictionary to store state transitions
22+
23+
# Iterate over all states in the monitor
24+
for s in range(0, monitor.num_states()):
25+
transitions[str(s)] = {} # Initialize transition mapping for the current state
26+
27+
# Iterate over all transitions from the current state
28+
for t in monitor.out(s):
29+
for ap in monitor.ap():
30+
ap = str(ap)
31+
bdd = buddy.bddtrue # Start with a true BDD (Boolean Decision Diagram)
32+
33+
# Build a BDD for the current atomic proposition
34+
for ap1 in monitor.ap():
35+
ap1 = str(ap1)
36+
if ap == ap1:
37+
p = monitor.register_ap(ap1)
38+
bdd = bdd & buddy.bdd_ithvar(p)
39+
else:
40+
p = monitor.register_ap(ap1)
41+
bdd = bdd & buddy.bdd_nithvar(p)
42+
43+
# Check if the transition condition is consistent with the BDD
44+
if (t.cond & bdd) != buddy.bddfalse:
45+
# Store the transition destination state for the current AP
46+
transitions[str(s)][ap] = str(t.dst)
47+
48+
# Build the CSP process model
49+
for s in transitions:
50+
csp += f'state{s} = \n' # Start defining the state process
51+
l = []
52+
for ap in transitions[s]:
53+
# Add the transition logic for each atomic proposition
54+
l.append(f'{ap} -> state{transitions[s][ap]}')
55+
csp += '\n[]\n'.join(l) # Join multiple transitions with non-deterministic choice
56+
csp += '\n\n'
57+
58+
# Add main process and verification conditions to the CSP model
59+
csp += f'WCST = state{monitor.get_init_state_number()} -- Main Process, starts the recursion in state{monitor.get_init_state_number()}\n\n'
60+
csp += f'assert state{monitor.get_init_state_number()}; RUN(Events) :[deadlock free]:\n'
61+
csp += f'assert state{monitor.get_init_state_number()} :[deterministic]:\n'
62+
csp += f'assert state{monitor.get_init_state_number()} :[divergence free]:'
63+
64+
return csp # Return the complete CSP model
65+
66+
# Function to convert an LTL formula into an RML (Reactive Model Logic) model
67+
def ltl2rml(ltl):
68+
rml = '' # Initialize the RML string
69+
# Translate the LTL formula to a monitor automaton using Spot
70+
monitor = spot.translate(ltl, 'monitor', 'det', 'complete')
71+
l = [] # List to store atomic propositions
72+
73+
# Build event matching rules for each atomic proposition
74+
for ap in monitor.ap():
75+
l.append(f'{ap} matches {{ event: \'{ap}\' }};')
76+
rml += '\n'.join(l) + '\n\n' # Add the rules to the RML string
77+
78+
transitions = {} # Dictionary to store state transitions
79+
80+
# Iterate over all states in the monitor
81+
for s in range(0, monitor.num_states()):
82+
transitions[str(s)] = {} # Initialize transition mapping for the current state
83+
84+
# Iterate over all transitions from the current state
85+
for t in monitor.out(s):
86+
for ap in monitor.ap():
87+
ap = str(ap)
88+
bdd = buddy.bddtrue # Start with a true BDD
89+
90+
# Build a BDD for the current atomic proposition
91+
for ap1 in monitor.ap():
92+
ap1 = str(ap1)
93+
if ap == ap1:
94+
p = monitor.register_ap(ap1)
95+
bdd = bdd & buddy.bdd_ithvar(p)
96+
else:
97+
p = monitor.register_ap(ap1)
98+
bdd = bdd & buddy.bdd_nithvar(p)
99+
100+
# Check if the transition condition is consistent with the BDD
101+
if (t.cond & bdd) != buddy.bddfalse:
102+
# Store the transition destination state for the current AP
103+
transitions[str(s)][ap] = str(t.dst)
104+
105+
# Build the RML process model
106+
for s in transitions:
107+
if s == str(monitor.get_init_state_number()):
108+
rml += 'Main = ' # Main process corresponds to the initial state
109+
else:
110+
rml += f'state{s} = ' # Define other states
111+
112+
l = []
113+
for ap in transitions[s]:
114+
# Add the transition logic for each atomic proposition
115+
if str(monitor.get_init_state_number()) == transitions[s][ap]:
116+
l.append(f'{ap} Main')
117+
else:
118+
l.append(f'{ap} state{transitions[s][ap]}')
119+
120+
rml += ' \/ '.join(l) # Join multiple transitions with choice operator
121+
rml += ';\n'
122+
123+
return rml # Return the complete RML model
124+
125+
# Main function to execute the script
126+
def main():
127+
# Set up argument parser
128+
parser = argparse.ArgumentParser(description='Convert an LTL formula into CSP and RML models.')
129+
parser.add_argument('ltl', help='The LTL formula to be converted.')
130+
parser.add_argument('--csp-output', default='monitor.csp', help='Output file for the CSP model (default: monitor.csp)')
131+
parser.add_argument('--rml-output', default='monitor.rml', help='Output file for the RML model (default: monitor.rml)')
132+
133+
# Parse the command line arguments
134+
args = parser.parse_args()
135+
136+
# Write the CSP model to a file
137+
with open(args.csp_output, 'w') as file:
138+
file.write(ltl2csp(args.ltl))
139+
140+
# Write the RML model to a file
141+
with open(args.rml_output, 'w') as file:
142+
file.write(ltl2rml(args.ltl))
143+
144+
print(f"CSP model written to {args.csp_output}")
145+
print(f"RML model written to {args.rml_output}")
146+
147+
# Entry point of the script
148+
if __name__ == '__main__':
149+
main()

0 commit comments

Comments
 (0)