Franck Pommereau / zinc

Go to a project
Toggle navigation Toggle navigation pinning
Franck Pommereau
fdb6809e 1 parent 99ddf22c

more code cleanup, bug located (hopefully)

Inline Side-by-side
Showing 3 changed files with 159 additions and 168 deletions
......@@ -13,7 +13,7 @@ func StateSpace (init func()Marking, addsucc func(Marking, Set),
for ! todo.Empty() {
state := todo.Get()
if print_states {
fmt.Println(*state)
fmt.Println(state)
}
succ = MakeSet()
addsucc(*state, succ)
......@@ -27,7 +27,7 @@ func StateSpace (init func()Marking, addsucc func(Marking, Set),
todo.Put(s)
}
if print_succs {
fmt.Println(" >", *s)
fmt.Println(" >", s)
}
}
}
......@@ -35,69 +35,70 @@ func StateSpace (init func()Marking, addsucc func(Marking, Set),
}
func DeadLocks (init func()Marking, addsucc func(Marking, Set), print bool) int {
// var succ Set
// count := 0
// i := init()
// todo := append(make([]*Marking, 0), &i)
// seen := MakeSet(i)
// for len(todo) > 0 {
// state := todo[0]
// todo = todo[1:]
// succ = MakeSet()
// addsucc(*state, succ)
// if succ.Empty() {
// if print {
// fmt.Printf("[%d] %s", count, state)
// }
// count += 1
// } else {
// for _, s := range *succ.data {
// if ! seen.Has(*s) {
// seen.Add(*s)
// todo = append(todo, s)
// }
// }
// }
// }
// return count
return 0
var succ Set
count := 1
i := init()
todo := MakeQueue(&i)
seen := MakeSet(&i)
for ! todo.Empty() {
state := todo.Get()
succ = MakeSet()
addsucc(*state, succ)
if succ.Empty() {
if print {
fmt.Println(state)
}
count++
} else {
for _, s := range succ.data {
if found, p := seen.Get(s); found {
s = p
} else {
s.SetId(seen.Len())
seen.AddPtr(s)
todo.Put(s)
}
}
}
}
return count
}
func LabelledTransitionsSystem (init func()Marking, itersucc SuccIterFunc) {
// count := 0
// i := init()
// todo := append(make([]*Marking, 0), &i)
// seen := MakeSet(i)
// for len(todo) > 0 {
// state := todo[0]
// todo = todo[1:]
// fmt.Printf("[%d] %s\n", count, state)
// count += 1
// for i, p := Iter(itersucc, *state); p != nil; p = i.Next() {
// // print trans & mode
// fmt.Print("@ ", p.Name, " = {")
// first := true
// for key, val := range p.Mode {
// if first {
// first = false
// } else {
// fmt.Print(", ")
// }
// fmt.Printf("'%s': ", key)
// fmt.Print(val)
// }
// fmt.Println("}")
// // print markings
// fmt.Println(" - ", p.Sub)
// fmt.Println(" + ", p.Add)
// s := state.Copy().Sub(p.Sub).Add(p.Add)
// fmt.Println(" > ", s)
// if ! seen.Has(s) {
// seen.Add(s)
// todo = append(todo, &s)
// }
// }
// }
i := init()
todo := MakeQueue(&i)
seen := MakeSet(&i)
for ! todo.Empty() {
state := todo.Get()
fmt.Println(state)
for i, p := Iter(itersucc, *state); p != nil; p = i.Next() {
// print trans & mode
fmt.Print("@ ", p.Name, " = {")
first := true
for key, val := range p.Mode {
if first {
first = false
} else {
fmt.Print(", ")
}
fmt.Printf("'%s': ", key)
fmt.Print(val)
}
fmt.Println("}")
// print markings
fmt.Println(" - ", p.Sub)
fmt.Println(" + ", p.Add)
s := state.Copy().Sub(p.Sub).Add(p.Add)
if found, old := seen.Get(&s); found {
fmt.Println(" > ", old)
} else {
s.SetId(seen.Len())
seen.Add(s)
todo.Put(&s)
fmt.Println(" > ", s)
}
}
}
}
func Main (name string, init func()Marking,
......@@ -115,6 +116,14 @@ func Main (name string, init func()Marking,
case "-g" : mode = GRAPH
case "-m" : mode = MARKS
case "-l" : mode = LTS
case "-ds" : mode = LOCKS; size = true
case "-gs" : mode = GRAPH; size = true
case "-ms" : mode = MARKS; size = true
case "-ls" : mode = LTS; size = true
case "-sd" : mode = LOCKS; size = true
case "-sg" : mode = GRAPH; size = true
case "-sm" : mode = MARKS; size = true
case "-sl" : mode = LTS; size = true
case "-h" :
fmt.Println("usage: ", name, " [-s] (-d|-g|-m|-l|-h)")
fmt.Println(" options:")
......
......@@ -7,64 +7,58 @@ from snakes.compil import ast, CompilationError
event = init = addsucc = itersucc = None
def statespace () :
"compute the marking graph"
todo = set([init()])
done = set()
succ = set()
g = collections.OrderedDict()
def dumpmarking (m) :
if hasattr(m, "ident") :
return "[%s] %s" % (m.ident, {p : list(t) for p, t in m.items()})
else :
return str({p : list(t) for p, t in m.items()})
def statespace (print_states, print_succs, print_dead) :
i = init()
i.ident = 0
todo = collections.deque([i])
seen = {i : 0}
dead = 0
while todo:
state = todo.pop()
done.add(state)
succ.clear()
state = todo.popleft()
succ = set()
addsucc(state, succ)
if state not in g :
g[state] = set()
g[state].update(succ)
succ.difference_update(done)
succ.difference_update(todo)
todo.update(succ)
return g
if not succ :
dead += 1
if (print_dead and not succ) or print_states :
print(dumpmarking(state))
for s in succ :
if s in seen :
s.ident = seen[s]
else :
s.ident = seen[s] = len(seen)
todo.append(s)
if print_succs :
print(" >", dumpmarking(s))
return len(seen), dead
def lts () :
"compute the labelled transition system (ie, detailled marking graph)"
todo = set([init()])
done = set()
succ = set()
g = collections.OrderedDict()
i = init()
i.ident = 0
todo = collections.deque([i])
seen = {i : 0}
while todo:
state = todo.pop()
done.add(state)
succ.clear()
for ev in itersucc(state) :
if state not in g :
g[state] = {}
if ev not in g[state] :
g[state][ev] = set()
s = state - ev.sub + ev.add
g[state][ev].add(s)
succ.add(s)
succ.difference_update(done)
succ.difference_update(todo)
todo.update(succ)
return g
def reachable (g=None):
"compute all the reachable markings"
if g is None :
g = statespace()
return set(g)
def deadlocks (g=None) :
"compute the set of deadlocks"
if g is None :
g = statespace()
return set(m for m, s in g.items() if not s)
state = todo.popleft()
print(dumpmarking(state))
for trans, mode, sub, add in itersucc(state) :
succ = state - sub + add
if succ in seen :
succ.ident = seen[succ]
else :
succ.ident = seen[succ] = len(seen)
todo.append(succ)
print("@ %s = %s" % (trans, mode))
print(" -", dumpmarking(sub))
print(" +", dumpmarking(add))
print(" >", dumpmarking(succ))
def main () :
import argparse
def dump (m) :
return repr({p : list(t) for p, t in m.items()})
parser = argparse.ArgumentParser()
parser.add_argument("-s", dest="size",
default=False, action="store_true",
......@@ -79,47 +73,29 @@ def main () :
group.add_argument("-d", dest="mode", action="store_const", const="d",
help="only print deadlocks")
args = parser.parse_args()
if args.mode == "l" and not args.size :
g = lts()
else :
g = statespace()
if args.mode in "gml" and args.size :
print("%s reachable states" % len(g))
n, _ = statespace(False, False, False)
print("%s reachable states")
elif args.mode == "d" and args.size :
print("%s deadlocks" % len(deadlocks(g)))
_, n = statespace(False, False, False)
print("%s deadlocks")
elif args.mode == "g" :
print("INIT ", dump(init()))
for num, (state, succ) in enumerate(g.items()) :
print("[%s]" % num, dump(state))
for s in succ :
print(">", dump(s))
elif args.mode in "md" :
print("INIT ", dump(init()))
if args.mode == "m" :
get = reachable
else :
get = deadlocks
for num, state in enumerate(get(g)) :
print("[%s]" % num, dump(state))
statespace(True, True, False)
elif args.mode in "m" :
statespace(True, False, False)
elif args.mode in "d" :
statespace(False, False, True)
elif args.mode == "l" :
for num, (state, events) in enumerate(g.items()) :
print("[%s]" % num, dump(state))
for ev, succ in events.items() :
print("@", repr(ev.trans), "=", ev.mode)
print(" -", dump(ev.sub))
print(" +", dump(ev.add))
for s in succ :
print(" >", dump(s))
lts()
class CodeGenerator (ast.CodeGenerator) :
def visit_Module (self, node) :
self.write("# %s\n\nNET = %r\n" % (self.timestamp(), node.name))
self.write("import itertools, collections")
self.children_visit(node.body)
self.write("\n%s" % inspect.getsource(dumpmarking))
self.write("\n%s" % inspect.getsource(statespace))
self.write("\n%s" % inspect.getsource(lts))
self.write("\n%s" % inspect.getsource(reachable))
self.write("\n%s" % inspect.getsource(deadlocks))
self.write("\n%s" % inspect.getsource(main))
self.write("\nif __name__ == '__main__':"
"\n main()")
......
import ast, collections
import collections
from snakes.tokens import Marking, mset, dot
from snakes.nets import Marking, mset, dot, hdict
def load_token (tok) :
if tok == {} :
return dot
return tok
event = collections.namedtuple("event", ["trans", "mode", "state"])
def load_state (text) :
text = text.replace("BlackToken()", "{}")
return Marking({place : mset(load_token(t) for t in tokens)
for place, tokens in ast.literal_eval(text).items()})
def load_code (text) :
return eval(text, {"dot": dot, "mset": mset})
def load_state (text, ident=None) :
m = Marking({place : mset(dot if t == {} else t for t in tokens)
for place, tokens in load_code(text).items()})
if ident is not None :
m.ident = ident
return m
def load (infile) :
g = {}
last = None
for line in infile :
try :
head, text = line.split(None, 1)
except :
raise ValueError("invalid line %r" % line)
state = load_state(text)
if head == "INIT" :
g[0] = state
elif head.startswith("[") :
if state in g :
print("duplicate state", state)
else :
g[state] = set()
last = state
elif head == ">>>" :
if state in g[last] :
print("duplicate succ", state)
g[last].add(state)
if head.startswith("[") :
ident = int(head[1:-1])
last = load_state(text, ident)
g[last] = set()
if ident == 0 :
g[0] = last
elif head == "@" :
trans, _, text = text.split(None, 2)
mode = hdict(load_code(text))
for k, v in mode.items() :
if isinstance(v, list) :
mode[k] = mset(v)
elif head in "+-" :
pass
elif head == ">" :
i, m = text.split(None, 1)
g[last].add(event(trans, mode, load_state(m, int(i[1:-1]))))
else :
raise ValueError("invalid line %r" % line)
return g
......@@ -48,13 +53,14 @@ def compare (left, right) :
seen = set(todo)
while todo :
state = todo.popleft()
todo.extend(left[state] - seen)
seen.update(left[state])
succs = set(e.state for e in left[state]) - seen
todo.extend(succs)
seen.update(succs)
if state not in right :
print("missing", state)
return
elif left[state] != right[state] :
print("not same successors for", state)
print("not same successors for [%s] %s" % (state.ident, state))
for s in left[state] - right[state] :
print(" -", s)
for s in right[state] - left[state] :
......