-
Notifications
You must be signed in to change notification settings - Fork 2
/
kid.py
executable file
·128 lines (105 loc) · 5.41 KB
/
kid.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
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
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
#!/usr/bin/env python3
import argparse
import logging
from LTL_to_atm.translator_via_spot import LTLToAtmViaSpot
from automata.k_reduction import k_reduce
from helpers.main_helper import setup_logging
from interfaces.LTL_to_automaton import LTLToAutomaton
from interfaces.spec import Spec
from module_generation.automaton_to_verilog import atm_to_verilog
from module_generation.verilog_to_aiger_via_yosys import verilog_to_aiger
from parsing.acacia_parser_helper import parse_acacia_and_build_expr
from parsing.tlsf_parser import convert_tlsf_or_acacia_to_acacia
from syntcomp.aiger_synthesizer import synthesize
from syntcomp.syntcomp_constants import REALIZABLE_RC, UNREALIZABLE_RC, print_syntcomp_unreal, print_syntcomp_unknown, \
UNKNOWN_RC, print_syntcomp_real
BAD_OUT_NAME = '__bad'
def _check_real(spec, is_moore, ltl_to_atm, min_k, max_k) -> str:
ucw_atm = ltl_to_atm.convert(~spec.formula)
logging.info("UCW automaton has %i states" % len(ucw_atm.nodes))
model_aiger = None
for k in range(min_k, max_k+1, 2):
logging.info("setting k to %i..." % k)
k_atm = k_reduce(ucw_atm, k)
logging.info("k-LA automaton has %i states" % len(k_atm.nodes))
# aiger_spec = v2a(atm_to_verilog(k_atm,
# spec.inputs, spec.outputs,
# 'automaton', BAD_OUT_NAME))
aiger_spec = verilog_to_aiger(atm_to_verilog(k_atm,
spec.inputs, spec.outputs,
'automaton', BAD_OUT_NAME))
model_aiger = synthesize(aiger_spec, is_moore, BAD_OUT_NAME)
if model_aiger:
return model_aiger
return model_aiger
def check_unreal(ltl_text:str, part_text:str, is_moore:bool,
ltl_to_atm:LTLToAutomaton,
min_k, max_k,
opt_level:int) -> str or None:
spec = parse_acacia_and_build_expr(ltl_text, part_text, ltl_to_atm, opt_level)
assert BAD_OUT_NAME not in (spec.inputs | spec.outputs), 'name collision'
neg_spec = Spec(spec.outputs, spec.inputs, ~spec.formula)
neg_is_moore = not is_moore
return _check_real(neg_spec, neg_is_moore, ltl_to_atm, min_k, max_k)
def check_real(ltl_text:str, part_text:str, is_moore:bool,
ltl_to_atm:LTLToAutomaton,
min_k:int,
max_k:int,
opt_level:int) -> str or None:
spec = parse_acacia_and_build_expr(ltl_text, part_text, ltl_to_atm, opt_level)
assert BAD_OUT_NAME not in (spec.inputs | spec.outputs), 'name collision'
return _check_real(spec, is_moore, ltl_to_atm, min_k, max_k)
def main():
parser = argparse.ArgumentParser(description='LTL synthesizer via k-reduction to AIGER',
formatter_class=argparse.ArgumentDefaultsHelpFormatter)
parser.add_argument('spec', metavar='spec', type=str,
help='TLSF or Wring (Acacia) spec file')
parser.add_argument('--minK', default=2, required=False, type=int,
help='min max number of visits to a bad state (within one SCC)')
parser.add_argument('--maxK', default=8, required=False, type=int,
help='max max number of visits to a bad state (within one SCC)')
parser.add_argument('-o', '--output', metavar='output', type=str,
help='output file for a model in the AIGER format (if not given -- print to stdout)')
group = parser.add_mutually_exclusive_group()
group.add_argument('--moore', action='store_true', default=False,
dest='moore',
help='system is Moore (ignored for TLSF)')
group.add_argument('--mealy', action='store_false',
default=True,
dest='moore',
help='system is Mealy (ignored for TLSF)')
parser.add_argument('--unreal', action='store_true', required=False,
help='check unrealizability: '
'negate the spec, system type, (in/out)puts, '
'and synthesize a model for the env '
'(note the spec will NOT be strengthened)')
parser.add_argument('-v', '--verbose', action='count', default=0,
help='verbosity level')
args = parser.parse_args()
setup_logging(args.verbose)
logging.info(args)
ltl_text, part_text, is_moore = convert_tlsf_or_acacia_to_acacia(args.spec, args.moore)
ltl_to_atm = LTLToAtmViaSpot()
if not args.unreal:
aiger_str = check_real(ltl_text, part_text, is_moore, ltl_to_atm, args.minK, args.maxK, 0)
if aiger_str is None:
print_syntcomp_unknown()
return UNKNOWN_RC
if args.output:
with open(args.output, 'w') as out:
out.write(aiger_str)
print_syntcomp_real(aiger_str)
return REALIZABLE_RC
else:
aiger_str = check_unreal(ltl_text, part_text, is_moore, ltl_to_atm, args.minK, args.maxK, 0)
if aiger_str:
logging.info('found model for env (not going to print it)')
# with open('/tmp/env.aag', 'w') as out:
# out.write(aiger_str)
print_syntcomp_unreal()
return UNREALIZABLE_RC
else:
print_syntcomp_unknown()
return UNKNOWN_RC
if __name__ == '__main__':
exit(main())