-
Notifications
You must be signed in to change notification settings - Fork 2
/
rally_kid_aiger.py
executable file
·75 lines (64 loc) · 2.5 KB
/
rally_kid_aiger.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
#!/usr/bin/env python3
import logging
import signal
from typing import List
import kid
from LTL_to_atm.translator_via_spot import LTLToAtmViaSpot
from syntcomp.rally_template import main_template
from syntcomp.task import Task
from syntcomp.task_creator import TaskCreator
class KidRealTask(Task):
def __init__(self, name,
ltl_text, part_text, is_moore,
min_k:int,
max_k:int,
formula_opt:int=0):
super().__init__(name, True)
self.name = name
self.ltl_text = ltl_text
self.part_text = part_text
self.is_moore = is_moore
self.min_k = min_k
self.max_k = max_k
self.formula_opt = formula_opt
def do(self):
return kid.check_real(self.ltl_text, self.part_text, self.is_moore,
LTLToAtmViaSpot(),
self.min_k, self.max_k,
self.formula_opt)
class KidUnrealTask(Task):
def __init__(self, name, ltl_text, part_text, is_moore,
min_k:int, max_k:int,
timeout):
super().__init__(name, False)
self.ltl_text = ltl_text
self.part_text = part_text
self.is_moore = is_moore
self.min_k = min_k
self.max_k = max_k
self.timeout = timeout
def do(self):
class TimeoutException(Exception):
pass
if self.timeout:
logging.info('CheckUnrealTask: setting timeout to %i' % self.timeout)
def signal_handler(sig, _):
if sig == signal.SIGALRM:
raise TimeoutException()
signal.signal(signal.SIGALRM, signal_handler)
signal.alarm(self.timeout)
try:
return kid.check_unreal(self.ltl_text, self.part_text, self.is_moore,
LTLToAtmViaSpot(),
self.min_k, self.max_k, 0)
except TimeoutException:
logging.debug('timeout reached')
return None
if __name__ == "__main__":
class KidTasksCreator(TaskCreator):
@staticmethod
def create(ltl_text:str, part_text:str, is_moore:bool) -> List[Task]:
return [KidRealTask('kid.real', ltl_text, part_text, is_moore, 4, 16),
KidUnrealTask('kid.unreal.short', ltl_text, part_text, is_moore, 2, 16, 1200)]
main_template("LTL synthesizer via AIGER, UCW -> k-LA -> AIGER, then solve with SDF solver",
KidTasksCreator())