-
Notifications
You must be signed in to change notification settings - Fork 2
/
ctl_to_ltl.py
executable file
·55 lines (39 loc) · 1.87 KB
/
ctl_to_ltl.py
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
#!/usr/bin/env python3
import argparse
import logging
from pprint import pformat
from CTL_to_LTL_ import ctlstar2ltl
from LTL_to_atm.ast_to_ltl3ba import ConverterToLtl2BaFormatVisitor
from LTL_to_atm.translator_via_spot import LTLToAtmViaSpot
from helpers.main_helper import setup_logging
from module_generation import spec_to_tlsf
from parsing.python_parser import parse_python_spec
def main() -> None:
parser = argparse.ArgumentParser(description='CTL* to LTL converter for synthesis',
formatter_class=argparse.ArgumentDefaultsHelpFormatter)
parser.add_argument('spec', metavar='spec', type=str,
help='the specification file (in python format)')
parser.add_argument('--k', default=None, type=int,
help='force the value of parameter k (the number of IDs)')
parser.add_argument('--out', '-o', default=None, type=str,
help='file name to output TLSF')
parser.add_argument('--log', metavar='log', type=str, required=False,
default=None,
help='name of the log file')
parser.add_argument('-v', '--verbose', action='count', default=0)
args = parser.parse_args()
setup_logging(args.verbose, args.log)
logging.info(args)
spec = parse_python_spec(args.spec)
logging.info('Input spec:\n' + str(spec))
new_spec = ctlstar2ltl.convert(spec, args.k, LTLToAtmViaSpot())
logging.info('introduced outputs:\n%s', pformat(new_spec.outputs - spec.outputs))
logging.info('LTL\n%s', ConverterToLtl2BaFormatVisitor().dispatch(new_spec.formula))
tlsf_str = spec_to_tlsf.convert(new_spec)
print(tlsf_str)
if args.out:
with open(args.out, 'w') as f:
f.write(tlsf_str)
logging.info("output TLSF is written to: " + args.out)
if __name__ == "__main__":
exit(main())