Showing
3 changed files
with
29 additions
and
8 deletions
... | @@ -77,13 +77,13 @@ class MakeLet (object) : | ... | @@ -77,13 +77,13 @@ class MakeLet (object) : |
77 | exec(match, env) | 77 | exec(match, env) |
78 | for name in set(env) - old : | 78 | for name in set(env) - old : |
79 | binding[name] = env[name] | 79 | binding[name] = env[name] |
80 | - def __call__ (self, __match__=None, __raise__=False, **args) : | 80 | + def __call__ (__self__, __match__=None, __raise__=False, **args) : |
81 | try : | 81 | try : |
82 | __binding__ = inspect.stack()[1][0].f_locals["__binding__"] | 82 | __binding__ = inspect.stack()[1][0].f_locals["__binding__"] |
83 | for name, value in args.items() : | 83 | for name, value in args.items() : |
84 | __binding__[name] = value | 84 | __binding__[name] = value |
85 | if __match__ : | 85 | if __match__ : |
86 | - self.match(__match__, __binding__) | 86 | + __self__.match(__match__, __binding__) |
87 | except : | 87 | except : |
88 | if __raise__ : | 88 | if __raise__ : |
89 | raise | 89 | raise | ... | ... |
1 | -import heapq | 1 | +import heapq, time |
2 | from snakes.nets import StateGraph | 2 | from snakes.nets import StateGraph |
3 | import snakes.lang | 3 | import snakes.lang |
4 | import snkast as ast | 4 | import snkast as ast |
5 | 5 | ||
6 | class Checker (object) : | 6 | class Checker (object) : |
7 | - def __init__ (self, net) : | 7 | + def __init__ (self, net, progress) : |
8 | + self.p = progress | ||
8 | self.g = StateGraph(net) | 9 | self.g = StateGraph(net) |
9 | self.f = [self.build(f) for f in net.label("asserts")] | 10 | self.f = [self.build(f) for f in net.label("asserts")] |
11 | + if progress : | ||
12 | + if len(self.f) == 0 : | ||
13 | + print("WARNING: no assertion given (computing the state space anyway)") | ||
14 | + elif len(self.f) == 1 : | ||
15 | + print("checking 1 assertion") | ||
16 | + else : | ||
17 | + print("checking %s assertions" % len(self.f)) | ||
10 | def build (self, tree) : | 18 | def build (self, tree) : |
11 | src = """ | 19 | src = """ |
12 | def check (_) : | 20 | def check (_) : |
... | @@ -14,25 +22,33 @@ def check (_) : | ... | @@ -14,25 +22,33 @@ def check (_) : |
14 | """ % tree.st.source()[7:] | 22 | """ % tree.st.source()[7:] |
15 | ctx = dict(self.g.net.globals) | 23 | ctx = dict(self.g.net.globals) |
16 | ctx["bounded"] = self.bounded | 24 | ctx["bounded"] = self.bounded |
25 | + ctx["dead"] = self.dead | ||
17 | exec(src, ctx) | 26 | exec(src, ctx) |
18 | fun = ctx["check"] | 27 | fun = ctx["check"] |
19 | fun.lineno = tree.lineno | 28 | fun.lineno = tree.lineno |
20 | return fun | 29 | return fun |
21 | def bounded (self, marking, max) : | 30 | def bounded (self, marking, max) : |
22 | return all(len(marking(p)) == 1 for p in marking) | 31 | return all(len(marking(p)) == 1 for p in marking) |
32 | + def dead (self) : | ||
33 | + return not bool(self.g.successors()) | ||
23 | def run (self) : | 34 | def run (self) : |
35 | + start = last = time.time() | ||
24 | for state in self.g : | 36 | for state in self.g : |
25 | marking = self.g.net.get_marking() | 37 | marking = self.g.net.get_marking() |
26 | for place in marking : | 38 | for place in marking : |
27 | if max(marking(place).values()) > 1 : | 39 | if max(marking(place).values()) > 1 : |
28 | - return None, self.trace(state) | 40 | + return len(self.g), None, self.trace(state) |
29 | for check in self.f : | 41 | for check in self.f : |
30 | try : | 42 | try : |
31 | if not check(marking) : | 43 | if not check(marking) : |
32 | - return check.lineno, self.trace(state) | 44 | + return len(self.g), check.lineno, self.trace(state) |
33 | except : | 45 | except : |
34 | pass | 46 | pass |
35 | - return None, None | 47 | + if self.p and time.time() - last >= 5 : |
48 | + last = time.time() | ||
49 | + print(" ... %s states explored so far in %.0f seconds" | ||
50 | + % (len(self.g), last - start)) | ||
51 | + return len(self.g), None, None | ||
36 | def path (self, tgt, src=0) : | 52 | def path (self, tgt, src=0) : |
37 | q = [(0, src, ())] | 53 | q = [(0, src, ())] |
38 | visited = set() | 54 | visited = set() | ... | ... |
... | @@ -87,6 +87,9 @@ opt.add_option("-a", "--all-names", | ... | @@ -87,6 +87,9 @@ opt.add_option("-a", "--all-names", |
87 | opt.add_option("--debug", | 87 | opt.add_option("--debug", |
88 | dest="debug", action="store_true", default=False, | 88 | dest="debug", action="store_true", default=False, |
89 | help="launch debugger on compiler error (default: no)") | 89 | help="launch debugger on compiler error (default: no)") |
90 | +opt.add_option("--progress", | ||
91 | + dest="progress", action="store_true", default=False, | ||
92 | + help="show progression during long operations (default: no)") | ||
90 | opt.add_option("-s", "--simul", | 93 | opt.add_option("-s", "--simul", |
91 | dest="simul", action="store_true", default=False, | 94 | dest="simul", action="store_true", default=False, |
92 | help="launch interactive code simulator") | 95 | help="launch interactive code simulator") |
... | @@ -295,7 +298,9 @@ def main (args=sys.argv[1:], src=None) : | ... | @@ -295,7 +298,9 @@ def main (args=sys.argv[1:], src=None) : |
295 | bug() | 298 | bug() |
296 | trace, lineno = [], None | 299 | trace, lineno = [], None |
297 | if options.check : | 300 | if options.check : |
298 | - lineno, trace = Checker(net).run() | 301 | + states, lineno, trace = Checker(net, options.progress).run() |
302 | + if options.progress : | ||
303 | + print("%s states explored" % states) | ||
299 | if options.simul : | 304 | if options.simul : |
300 | engine = "dot" | 305 | engine = "dot" |
301 | for eng in gv_engines : | 306 | for eng in gv_engines : | ... | ... |
-
Please register or login to post a comment