Commit f9f35e07 authored by Andrew's avatar Andrew
Browse files

Fixing bugs with tree automata. Added corresponding tests.

parent 5a8b3d3d
This diff is collapsed.
import itertools
from collections import namedtuple
class Pipeline:
def __init__(self, in_type):
......@@ -20,10 +21,10 @@ class Pipeline:
def check_valid(self):
if not self.process_list:
return True
if not self.in_type.is_subtype(self.process_list[0]):
if not self.in_type.is_subtype(self.process_list[0].in_type):
return False
for p1, p2 in zip(self.process_list[:-1], self.process_list[1:]):
if not p1.out_type.is_subtype(p2.in_type):
if not p2.in_type.is_subtype(p1.out_type):
return False
for i, p1 in enumerate(self.process_list):
for p2 in self.process_list[i+1:]:
......@@ -33,7 +34,6 @@ class Pipeline:
return False
return True
class Process:
def __init__(self, in_type, out_type):
......@@ -49,6 +49,9 @@ class DataType:
self._var_value_dict = {k: frozenset(v) for k, v in var_value_dict.items()}
self.TupleClass = namedtuple('datatype', var_value_dict.keys())
def __str__(self):
return str(tuple(self.var_names()))
def __call__(self, **kwargs):
return self.TupleClass(**kwargs)
......@@ -108,12 +111,6 @@ class DataType:
for o_val in itertools.product(*[self.var_values(name) for name in new_names]):
yield self.TupleClass(**(val_dict | dict(zip(new_names, o_val))))
'''
def possible_values(self):
values = itertools.product(*[self.var_values(name) for name in self.var_names()])
return {self.TupleClass._make(val) for val in values}
'''
def from_subvalues(self, *subvalues):
return self(**{k: v for sv in subvalues for k, v in sv._asdict().items()})
......@@ -136,5 +133,11 @@ class DataType:
def is_empty_type(self):
return len(self.var_names()) == 0
def from_ordered_values(self, values):
if not type(values) == list and not type(values) == tuple:
values = (values,)
return self(**dict(zip(self.var_names(), values)))
empty_type = DataType({})
empty_value = empty_type()
import dist_process
from DESops.tree import dist_process
def pipeline_synthesis(pipe, spec_ata, delay=False):
def pipeline_synthesis(pipe, spec_ata):
"""
Perform synthesis on a pipeline architecture for the given specification automaton
The automaton should have input type given by the non-environmental (input) variables of the pipeline
......@@ -16,7 +16,7 @@ def pipeline_synthesis(pipe, spec_ata, delay=False):
for i, p in enumerate(pipe.process_list):
print(f"Reducing process {i}")
# Narrow the directions of the specification to the input of the current process
A.append(B[-1].narrow(p.in_type).copy_int())
A.append(B[-1].narrow_direction(p.in_type).copy_int())
# Make the result nondeterministic for change operation / nonemptiness check
N.append(A[-1].to_nondet().copy_int())
# No need to compute change operation for last process
......@@ -24,15 +24,29 @@ def pipeline_synthesis(pipe, spec_ata, delay=False):
break
# Nondeterministically implement the current process
# Change the direction type of the specification to the output of the current process
B.append(N[-1].change_pipeline(p.out_type, delay=delay).copy_int())
B.append(N[-1].change_pipeline(p.out_type).copy_int())
# check emptiness for last automaton and find an implementation if one exists
print("Checking emptiness")
empty, member_ata = N[-1].is_empty()
return empty
if empty:
return {"realizable": not empty, "solution": None}
realizable = not N[-1].is_empty()
return realizable, N
def construct_pipeline_realization(pipe, N):
strats = []
previous = None
for i, joint_ata in reversed(enumerate(N)):
if i < len(N):
joint_ata = joint_ata.AND(previous.inverse_change())
winning_set = joint_ata.construct_winning_set_emptiness()
joint_strat = joint_ata.construct_tree_element(winning_set)
strat = joint_strat.narrow_input(pipe.process_list[i].out_type)
strats.append(strat)
previous = joint_strat
"""
# iterate and find implementation for the previous processes
ata_list = [member_ata]
lifted_ata_list = [member_ata]
......@@ -54,37 +68,24 @@ def pipeline_synthesis(pipe, spec_ata, delay=False):
"""
def linear_to_tree_specification(g, dir_type, mode="mealy"):
if mode == "mealy":
delay = False
elif mode == "moore":
delay = True
else:
raise ValueError("Mode must be mealy/moore")
return g.change_pipeline(dir_type, mode='AND', delay=delay)
def linear_to_tree_specification_pipeline(g, pipe):
def pipeline_linear_to_tree_spec(pipe, awa, delay=False):
"""
This method takes the word automaton g and appropriately shifts variables according to the pipeline arch
This method takes the word automaton awa and appropriately shifts variables according to the pipeline arch
so that strategies composed with delay have traces accepted by the shifted version correspond
to strategies composed without delay have traces accepted by g.
This method then takes this shifted word automaton and converts it into a tree automaton
with directions given by the input to the architecture
TODO - for efficiency, shifting should be done inbetween each step of synthesis rather than all at the beginning
"""
empty_type = dist_process.empty_type
augmented_output_types = [empty_type.product_type(*[proc.out_type for proc in pipe.process_list[i:]])
for i in range(len(pipe.process_list))]
# TODO this is buggy
"""
for t1, t2 in zip(augmented_output_types[:-1], augmented_output_types[1:]):
g = g.delay_in(t1)
g = g.delay_in(t2)
"""
for t in augmented_output_types:
g = g.delay_in(t)
# TODO - for efficiency, shifting should be done inbetween each step of synthesis rather than all at the beginning
ata = awa
if not delay:
delay_type = dist_process.empty_type
# delay the outputs of the nth the last process by n
for proc in reversed(pipe.process_list):
delay_type = delay_type.product_type(proc.out_type)
ata = ata.delay_in(delay_type)
return ata.change_pipeline(pipe.in_type, mode="AND")
return g.change_pipeline(pipe.in_type, mode='AND', delay=False)
class SCCHelper:
def __init__(self, nfa):
self.nfa = nfa
self.time = 0
self.stack = []
self.nfa.vs["visitTime"] = -1
self.nfa.vs["lowTime"] = -1
self.nfa.vs["inStack"] = False
self.sccList = []
def computeSCC(self):
"""
Compute the strongly connected components of the ATA viewed as a directed graph.
Result guaranteed to be in reverse topological order.
"""
for q in self.nfa.vs:
if q["visitTime"] < 0:
self.computePointedSCC(q)
return self.sccList
def computePointedSCC(self, q):
q["visitTime"] = self.time
q["lowTime"] = self.time
self.time += 1
self.stack.append(q)
q["inStack"] = True
for s in q.neighbors(mode="out"):
if s["visitTime"] < 0:
self.computePointedSCC(s)
q["lowTime"] = min(q["lowTime"], s["lowTime"])
elif s["inStack"]:
q["lowTime"] = min(q["lowTime"], s["visitTime"])
if q["lowTime"] == q["visitTime"]:
s = None
scc = set()
while q != s:
s = self.stack.pop()
s["inStack"] = False
scc.add(s["name"])
self.sccList.append(scc)
......@@ -2,13 +2,12 @@ import DESops.tree.ATA as ATA
import DESops.tree.ATA as ASA
import DESops.tree.dist_process as dist_process
import DESops.tree.dist_synthesis as dist_synthesis
from DESops.tree.dist_process import empty_type, empty_value
import DESops
from DESops import NFA
from itertools import chain
empty_type = dist_process.DataType({})
empty_val = empty_type()
def inferability(pipe):
......@@ -146,7 +145,7 @@ def create_dist_problem(g, info_attr="info"):
A_plant_dyn = plant_dyn(pipe, g).complement().simplify()
A_spec = A_block_guarantee.AND((A_inf.AND(A_sec)).OR(A_block_assumption, A_plant_dyn)).simplify()
A_spec = A_spec.widen_output(master_type)
A_spec = A_spec.widen_input(master_type)
#A_spec = dist_synthesis.linear_to_tree_specification(A_spec, pipe.in_type, mode="mealy")
A_spec = dist_synthesis.linear_to_tree_specification_pipeline(A_spec, pipe)
......
from DESops.tree import ATA, dist_process, dist_synthesis
from DESops.automata import DFA
empty_type = dist_process.DataType({})
empty_val = empty_type()
def match_spec():
in_type = dist_process.DataType({'p_out': {1,2}})
dir_type = dist_process.DataType({'p_in': {1,2}})
ata_inf = ATA.ATA(in_type, dir_type)
ata_inf.add_states({"q"})
ata_inf.init_state = "q"
ata_inf.add_transitions({("q", in_type(p_out=info)):
ata_inf.alg.Symbol(("q", dir_type(p_in=info)))
for info in {1,2}})
ata_inf.set_weak_buchi(ata_inf.states)
return ata_inf
def lin_match_spec():
in_type = dist_process.DataType({'y':{0,1}, 'x':{0,1}, 'p_out': {0,1}, 'p_in': {0,1}})
ata_inf = ATA.AWA(in_type.subtype(['p_in', 'p_out']))
ata_inf.add_states({0})
ata_inf.init_state = 0
ata_inf.add_transitions({(0, ata_inf.in_type(p_out=info, p_in=info)):
ata_inf.alg.Symbol((0, dist_process.empty_value))
for info in {0,1}})
ata_inf.set_weak_buchi(ata_inf.states)
ata_o = ATA.AWA(in_type.subtype(['x', 'p_in']))
ata_o.add_states({0})
ata_o.init_state = 0
ata_o.add_transitions({(0, ata_o.in_type(p_in=info, x=1-info)):
ata_o.alg.Symbol((0, dist_process.empty_value))
for info in {0, 1}})
ata_o.set_weak_buchi(ata_o.states)
ata_o.complement()
ata_inf = ata_inf.OR(ata_o).widen_output(in_type)
return ata_inf
def lin_match_spec_2():
in_type = dist_process.DataType({'x':{0,1}, 'p_out': {0,1}, 'p_in': {0,1}})
ata_inf = ATA.AWA(in_type.subtype(['p_in', 'p_out']))
ata_inf.add_states({0})
ata_inf.init_state = 0
ata_inf.add_transitions({(0, ata_inf.in_type(p_out=info, p_in=info)):
ata_inf.alg.Symbol((0, dist_process.empty_value))
for info in {0,1}})
ata_inf.set_weak_buchi(ata_inf.states)
return ata_inf.widen_output(in_type)
def lin_spec():
in_type = dist_process.DataType({'p_out': {0, 1}, 'p_in': {0, 1}})
ata_inf = ATA.AWA(in_type)
ata_inf.add_states({0, 1, 2})
ata_inf.init_state = 0
ata_inf.add_transitions({(0, ata_inf.in_type(p_out=0, p_in=1)):
ata_inf.alg.Symbol((1, dist_process.empty_value))})
ata_inf.add_transitions({(0, ata_inf.in_type(p_out=0, p_in=0)):
ata_inf.alg.Symbol((2, dist_process.empty_value))})
ata_inf.add_transitions({(1, ata_inf.in_type(p_out=1, p_in=0)):
ata_inf.alg.Symbol((1, dist_process.empty_value))})
ata_inf.add_transitions({(2, ata_inf.in_type(p_out=0, p_in=1)):
ata_inf.alg.Symbol((2, dist_process.empty_value))})
ata_inf.add_transitions({(1, ata_inf.in_type(p_out=1, p_in=1)):
ata_inf.alg.Symbol((1, dist_process.empty_value))})
ata_inf.add_transitions({(2, ata_inf.in_type(p_out=0, p_in=0)):
ata_inf.alg.Symbol((2, dist_process.empty_value))})
ata_inf.set_weak_buchi(ata_inf.states)
return ata_inf
"""
A = match_spec()
print(A.is_nondet())
#print(A.transitions)
#A = A.to_nondet()
#print(A.transitions)
empty, tree = A.is_empty()
#print(tree.transitions)
"""
A = lin_match_spec_2()
A.simplify()
#A_tree = dist_synthesis.linear_to_tree_specification(A, A.in_type.subtype(['p_in']), mode="mealy")
pipe = dist_process.Pipeline(A.in_type.subtype({"p_in"}))
p1 = dist_process.Process(
A.in_type.subtype({"p_in"}),
A.in_type.subtype({"x"})
)
pipe.append_process(p1)
p2 = dist_process.Process(
A.in_type.subtype({"x"}),
A.in_type.subtype({"p_out"})
)
pipe.append_process(p2)
A_spec = dist_synthesis.linear_to_tree_specification_pipeline(A, pipe)
res = dist_synthesis.pipeline_synthesis(pipe, A_spec, delay=True)
print(res)
"""
#print(A_tree.transitions)
#print(A_tree.is_empty())
#print(A_tree.is_nondet())
B = A_tree.delay_in(p2.out_type)
#print(B.transitions)
#print(B.is_empty())
C = B.delay_in(A_tree.in_type)
print(C.transitions)
print(C.is_empty())
D = B.change_pipeline(p1.out_type, delay=True)
print(D.transitions)
print(D.to_nondet().is_empty())
#B = A_tree.change_pipeline(p1.out_type, delay=False)
#print(B.transitions)
#print(B.to_nondet().is_empty())
res = dist_synthesis.pipeline_synthesis(pipe, A_tree, delay=False)
print(res)
"""
"""
B=A
#B = A.delay_in(A.in_type.quotient_type(pipe.in_type))
C = B.delay_in(A.in_type.quotient_type(pipe.in_type))
print("HEHHE")
print(A.in_type.quotient_type(pipe.in_type).var_names())
D = C.delay_in(p2.out_type)
print(p2.out_type.var_names())
#E = D.change_pipeline(pipe.in_type, mode='AND', delay=True)
#F = E.to_nondet().change_pipeline(p1.out_type, mode='OR', delay=True).copy_int()
#print(F.init_state)
#print(F.transitions)
#print(F.to_nondet().is_empty())
A_tree = dist_synthesis.linear_to_tree_specification(D, pipe.in_type)
res = dist_synthesis.pipeline_synthesis(pipe, A_tree, delay=True)
print(res)
"""
"""
A = lin_spec()
A = A.to_tree_automaton(A.in_type.subtype(['p_in']))
#A = A.delay_input_mod()
A = A.to_nondet()
#A = A.change_pipeline(A.in_type)
print(A.transitions)
empty, B = A.is_empty()
print(empty)
print(A.accepts_tree(B))
"""
from DESops.tree import ATA, dist_process
def ata_example1():
in_type = dist_process.DataType({'p_out': {1, 2}})
dir_type = dist_process.DataType({'p_in': {1, 2}})
ata = ATA.ATA(in_type, dir_type)
ata.add_states({0, 1, 2, 3})
ata.init_state = 0
ata.add_simple_transitions({(0, 1): [],
(0, 2): [[(1, 1), (2, 1)]],
(1, 1): [[(3, 1)]],
(2, 1): [[(2, 2)]],
(2, 2): [[(3, 1)]],
(3, 1): [[(3, 1)]]})
ata.set_weak_buchi({3})
ata.simplify()
return ata
def ata_example2():
in_type = dist_process.DataType({'p_out': {1, 2}})
dir_type = dist_process.DataType({'p_in': {1, 2}})
ata = ATA.ATA(in_type, dir_type)
ata.add_states({0, 1})
ata.init_state = 0
ata.add_simple_transitions({(0, 2): [[(1, 1), (1, 2)]],
(1, 1): [[(1, 1), (0, 2)]]})
ata.set_weak_buchi({0,1})
ata.simplify()
return ata
def ata_example3():
in_type = dist_process.DataType({'p_out': {1, 2}})
dir_type = dist_process.DataType({'p_in': {1, 2}})
ata = ATA.ATA(in_type, dir_type)
ata.add_states({0, 1})
ata.init_state = 0
ata.add_simple_transitions({(0, 2): [[(1, 1), (1, 2)]],
(1, 2): [[(1, 1), (0, 2)]]})
ata.set_weak_buchi({0,1})
ata.simplify()
return ata
def test_ATA():
ata = ata_example1()
assert len(ata.states) == 4
def test_weak_buchi():
weak_ata = ata_example1()
assert weak_ata.is_weak_buchi()
non_weak_ata = ata_example1()
non_weak_ata.add_simple_transitions({(3, 1): [[(0, 1)]]})
assert not non_weak_ata.is_weak_buchi()
def test_nondet():
ata = ata_example1()
assert not ata.is_nondet()
assert ata.to_nondet().is_nondet()
assert ata.complement().is_nondet()
def test_emptiness():
ata = ata_example1().to_nondet()
empty, winning = ata.test_emptiness()
assert not empty
assert ata.construct_tree_element(winning).is_tree()
ata.set_weak_buchi({0})
assert ata.to_nondet().is_empty()
def test_lang_subset():
ata1 = ata_example1()
ata2 = ata_example1()
ata2.add_simple_transitions({(1, 2): [[(3, 1)]]})
assert ata1.is_language_subset(ata2)
assert not ata2.is_language_subset(ata1)
def test_tree():
ata = ata_example1()
assert not ata.is_tree()
tree_ata = ata_example2()
assert tree_ata.is_tree()
assert ata.accepts_tree(tree_ata)
tree_ata = ata_example3()
assert tree_ata.is_tree()
assert not ata.accepts_tree(tree_ata)
def ata_example4():
# accepts p0-trees where inputs p1 and p2 match
in_type = dist_process.DataType({'p1': {1, 2}, 'p2': {1, 2}})
dir_type = dist_process.DataType({'p0': {1, 2}})
ata = ATA.ATA(in_type, dir_type)
ata.add_states({0})
ata.init_state = 0
ata.add_simple_transitions({(0, (1, 1)): [[(0, 1), (0, 2)]],
(0, (2, 2)): [[(0, 1), (0, 2)]]})
ata.set_weak_buchi({0})
ata.simplify()
return ata
def ata_example5():
# accepts p0-trees where input p2 matches previous input p1, first p1 must be 1
in_type = dist_process.DataType({'p1': {1, 2}, 'p2': {1, 2}})
dir_type = dist_process.DataType({'p0': {1, 2}})
ata = ATA.ATA(in_type, dir_type)
ata.add_states({0, 1})
ata.init_state = 0
ata.add_simple_transitions({(0, (1, 1)): [[(0, 1), (0, 2)]],
(0, (2, 1)): [[(1, 1), (1, 2)]],
(1, (1, 2)): [[(0, 1), (0, 2)]],
(1, (2, 2)): [[(1, 1), (1, 2)]]})
ata.set_weak_buchi({0, 1})
ata.simplify()
return ata
def ata_example6():
# accepts words where inputs p1 and p2 match
in_type = dist_process.DataType({'p0': {1, 2}, 'p1': {1, 2}, 'p2': {1, 2}})
dir_type = dist_process.empty_type
ata = ATA.ATA(in_type, dir_type)
ata.add_states({0})
ata.init_state = 0
ata.add_simple_transitions({(0, (1, 1, 1)): [[(0, ())]],
(0, (1, 2, 2)): [[(0, ())]],
(0, (2, 1, 1)): [[(0, ())]],
(0, (2, 2, 2)): [[(0, ())]]})
ata.set_weak_buchi({0})
ata.simplify()
return ata
def test_change_pipeline():
ata4 = ata_example4()
ata5 = ata_example5()
ata6 = ata_example6()
t0 = ata4.dir_type
t1 = ata4.in_type.subtype({'p1'})
t2 = ata4.in_type.subtype({'p2'})
# in each step, we can choose p1 to match p2
assert not ata4.change_pipeline(t1).to_nondet().is_empty()
# in each step, environment can choose p1 to not match p2
assert ata4.change_pipeline(t1, mode="AND").to_nondet().is_empty()
# ata5 accepts the trees of ata4 whose first input has p1=1
#ata4_delay = ata4.delay_in(t2)
#assert ata5.is_language_subset(ata4_delay)
#assert not ata4_delay.is_language_subset(ata5)
# in each step, for any environment choice of p1, we can choose p2 to match in the next step
assert not ata5.change_pipeline(t1, mode="AND").to_nondet().is_empty()
# ata4 accepts all trees whose paths are accepted by ata6
ata6_change = ata6.change_pipeline(t0, mode="AND")
assert ata6_change.is_language_equivalent(ata4)
from DESops.tree import ATA, dist_process, dist_synthesis
def test_types():
pass
def test_pipeline():
super_type = dist_process.DataType({'p0': {0, 1}, 'p1': {"x", "y"},
'p2': {frozenset({4}), frozenset({5})}, 'p3': {1, "2"}})
pipe = dist_process.Pipeline(super_type.subtype({"p0"}))
p1 = dist_process.Process(
super_type.subtype({"p0"}),
super_type.subtype({"p1", "p2"})
)
pipe.append_process(p1)
p2 = dist_process.Process(
super_type.subtype(({"p1"})),
super_type.subtype(({"p3"}))
)
pipe.append_process(p2)
assert pipe.check_valid()
def match_spec(t1, t2, match_pairs):
match = lambda v1, v2: all(getattr(v1, s1) == getattr(v2, s2) for s1, s2 in match_pairs)
super_type = t1.product_type(t2)
ata = ATA.ATA(super_type, dist_process.empty_type)
ata.add_states({"q"})
ata.init_state = "q"
ata.add_transitions({("q", super_type.from_subvalues(v1, v2)):
ata.alg.Symbol(("q", dist_process.empty_value))
for v1 in t1 for v2 in t2 if match(v1, v2)})
ata.set_weak_buchi(ata.states)
return ata
def test_match_pipeline():