# -*- coding: utf-8 -*-
## Filename : TestMCLTranslators.py
## Author(s) : Michel Le Borgne
## Created : 9 mars 2012
## Revision :
## Source :
##
## Copyright 2012 - 2020 IRISA/IRSET
##
## This library is free software; you can redistribute it and/or modify it
## under the terms of the GNU General Public License as published
## by the Free Software Foundation; either version 2.1 of the License, or
## any later version.
##
## This library is distributed in the hope that it will be useful, but
## WITHOUT ANY WARRANTY, WITHOUT EVEN THE IMPLIED WARRANTY OF
## MERCHANTABILITY OR FITNESS FOR A PARTICULAR PURPOSE. The software and
## documentation provided here under is on an "as is" basis, and IRISA has
## no obligations to provide maintenance, support, updates, enhancements
## or modifications.
## In no event shall IRISA be liable to any party for direct, indirect,
## special, incidental or consequential damages, including lost profits,
## arising out of the use of this software and its documentation, even if
## IRISA have been advised of the possibility of such damage. See
## the GNU General Public License for more details.
##
## You should have received a copy of the GNU General Public License
## along with this library; if not, write to the Free Software Foundation,
## Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA.
##
## The original code contained here was initially developed by:
##
## Michel Le Borgne.
## IRISA
## Symbiose team
## IRISA Campus de Beaulieu
## 35042 RENNES Cedex, FRANCE
##
##
## Contributor(s):
##
"""
Unitary tests for the translators
"""
from __future__ import print_function
import pkg_resources
import unittest
from cadbiom.models.clause_constraints.CLDynSys import CLDynSys
from cadbiom.models.clause_constraints.mcl.MCLTranslators import (
MCLSigExprVisitor,
gen_transition_clock,
gen_transition_list_clock,
gen_simple_evolution,
GT2Clauses,
)
from cadbiom.models.biosignal.sig_expr import (
SigIdentExpr,
SigSyncBinExpr,
SigWhenExpr,
SigDefaultExpr,
)
from cadbiom.models.guard_transitions.chart_model import ChartModel
from cadbiom.models.guard_transitions.analyser.ana_visitors import TableVisitor
from cadbiom.models.clause_constraints.mcl.MCLAnalyser import MCLAnalyser
[docs]class ErrorRep(object):
"""Simple error reporter"""
def __init__(self):
self.mess = ""
self.error = False
[docs] def display(self, mess):
"""
set error and print
"""
self.error = True
self.mess += ">> " + mess
print(" DISPLAY CALL>> " + mess)
[docs]class TestTransitionClauses(unittest.TestCase):
"""
Test of transitions into clauses
"""
[docs] def test_no_cond(self): # OK
"""
n1 --> n2; []
"""
model = ChartModel("Test")
root = model.get_root()
nn1 = root.add_simple_node("n1", 0, 0)
nn2 = root.add_simple_node("n2", 0, 0)
trans = root.add_transition(nn1, nn2)
tvisit = TableVisitor(None) # no error display
model.accept(tvisit)
reporter = ErrorRep()
cl_ds = CLDynSys(tvisit, reporter)
event_literal = gen_transition_clock(trans, cl_ds, None, reporter)
print("Transition clock:", str(event_literal))
assert str(event_literal) == "n1"
assert cl_ds.clauses == []
print("free clocks registered:", cl_ds.free_clocks)
assert cl_ds.free_clocks == []
print("reporter:", reporter.mess)
assert reporter.mess == ""
[docs] def test_cond(self): # OK
"""
n1 --> n2; [not n3]
"""
model = ChartModel("Test")
root = model.get_root()
nn1 = root.add_simple_node("n1", 0, 0)
nn2 = root.add_simple_node("n2", 0, 0)
root.add_simple_node("n3", 0, 0)
trans = root.add_transition(nn1, nn2)
trans.set_condition("not n3")
tvisit = TableVisitor(None) # no error display
model.accept(tvisit)
reporter = ErrorRep()
cl_ds = CLDynSys(tvisit.tab_symb, None)
event_literal = gen_transition_clock(trans, cl_ds, None, reporter)
print("Transition clock:", str(event_literal))
assert str(event_literal) == "_lit0"
expected = ["$n1, not _lit0$", "$not n3, not _lit0$", "$not n1, n3, _lit0$"]
assert [str(clause) for clause in cl_ds.clauses] == expected
print("free clocks registered:", cl_ds.free_clocks)
assert cl_ds.free_clocks == []
print("reporter:", reporter.mess)
assert reporter.mess == ""
[docs] def test_no_cond_event(self): # OK
"""
n1 --> n2; h[]
"""
model = ChartModel("Test")
root = model.get_root()
nn1 = root.add_simple_node("n1", 0, 0)
nn2 = root.add_simple_node("n2", 0, 0)
trans = root.add_transition(nn1, nn2)
trans.set_event("h")
tvisit = TableVisitor(None) # no error display
model.accept(tvisit)
reporter = ErrorRep()
cl_ds = CLDynSys(tvisit.tab_symb, reporter)
event_literal = gen_transition_clock(trans, cl_ds, None, reporter)
print("Transition clock:", str(event_literal))
assert str(event_literal) == "_lit0"
expected = ["$not _lit0, h$", "$not _lit0, n1$", "$not h, not n1, _lit0$"]
assert [str(clause) for clause in cl_ds.clauses] == expected
print("free clocks registered:", cl_ds.free_clocks)
assert cl_ds.free_clocks == ["h"]
print("reporter: ", reporter.mess)
assert reporter.mess == ""
print("---------- opti ----------------")
sed = dict()
tvisit = TableVisitor(None) # no error display
model.accept(tvisit)
cl_ds = CLDynSys(tvisit.tab_symb, reporter)
event_literal = gen_transition_clock(trans, cl_ds, sed, reporter)
print("Transition clock:", str(event_literal))
assert str(event_literal) == "_lit0"
assert [str(clause) for clause in cl_ds.clauses] == expected
print("free clocks registered:", cl_ds.free_clocks)
assert cl_ds.free_clocks == ["h"]
print("reporter: ", reporter.mess)
assert reporter.mess == ""
[docs] def test_cond_event(self): # OK
"""
n1 --> n2; h[not n3]
"""
model = ChartModel("Test")
root = model.get_root()
nn1 = root.add_simple_node("n1", 0, 0)
nn2 = root.add_simple_node("n2", 0, 0)
root.add_simple_node("n3", 0, 0)
trans = root.add_transition(nn1, nn2)
trans.set_condition("not n3")
trans.set_event("h")
tvisit = TableVisitor(None) # no error display
model.accept(tvisit)
reporter = ErrorRep()
cl_ds = CLDynSys(tvisit.tab_symb, None)
event_literal = gen_transition_clock(trans, cl_ds, None, reporter)
print("Transition clock:", str(event_literal))
assert str(event_literal) == "_lit1"
expected = [
"$n1, not _lit0$",
"$not n3, not _lit0$",
"$not n1, n3, _lit0$",
"$not _lit1, h$",
"$not _lit1, _lit0$",
"$not h, not _lit0, _lit1$",
]
assert [str(clause) for clause in cl_ds.clauses] == expected
print("free clocks registered:", cl_ds.free_clocks)
assert cl_ds.free_clocks == ["h"]
print("reporter: ", reporter.mess)
assert reporter.mess == ""
print("---------- opti ----------------")
sed = dict()
tvisit = TableVisitor(None) # no error display
model.accept(tvisit)
reporter = ErrorRep()
cl_ds = CLDynSys(tvisit.tab_symb, None)
event_literal = gen_transition_clock(trans, cl_ds, sed, reporter)
print("Transition clock:", str(event_literal))
assert str(event_literal) == "_lit1"
assert [str(clause) for clause in cl_ds.clauses] == expected
print("free clocks registered:", cl_ds.free_clocks)
assert cl_ds.free_clocks == ["h"]
print("reporter: ", reporter.mess)
assert reporter.mess == ""
[docs] def test_perm_no_cond_event(self): # OK
"""
n1/p --> n2; h[];
"""
model = ChartModel("Test")
root = model.get_root()
nn1 = root.add_perm_node("n1", 0, 0)
nn2 = root.add_simple_node("n2", 0, 0)
trans = root.add_transition(nn1, nn2)
trans.set_event("h")
tvisit = TableVisitor(None) # no error display
model.accept(tvisit)
reporter = ErrorRep()
cl_ds = CLDynSys(tvisit.tab_symb, None)
event_literal = gen_transition_clock(trans, cl_ds, None, reporter)
print("Transition clock:", str(event_literal))
assert str(event_literal) == "_lit0"
expected = ["$not _lit0, h$", "$not _lit0, n1$", "$not h, not n1, _lit0$"]
assert [str(clause) for clause in cl_ds.clauses] == expected
print("free clocks registered:", cl_ds.free_clocks)
assert cl_ds.free_clocks == ["h"]
print("reporter: ", reporter.mess)
assert reporter.mess == ""
[docs] def test_perm_cond_event(self): # OK
"""
n4;
n1/p --> n2; h[n4];
"""
model = ChartModel("Test")
root = model.get_root()
nn1 = root.add_perm_node("n1", 0, 0)
nn2 = root.add_simple_node("n2", 0, 0)
root.add_simple_node("n4", 0, 0)
trans = root.add_transition(nn1, nn2)
trans.set_condition("n4")
trans.set_event("h")
tvisit = TableVisitor(None) # no error display
model.accept(tvisit)
reporter = ErrorRep()
cl_ds = CLDynSys(tvisit.tab_symb, None)
event_literal = gen_transition_clock(trans, cl_ds, None, reporter)
print("Transition clock:", str(event_literal))
assert str(event_literal) == "_lit0"
expected = ["$not _lit0, h$", "$not _lit0, n4$", "$not h, not n4, _lit0$"]
assert [str(clause) for clause in cl_ds.clauses] == expected
print("free clocks registered:", cl_ds.free_clocks)
assert cl_ds.free_clocks == ["h"]
print("reporter: ", reporter.mess)
assert reporter.mess == ""
# complex events
[docs] def test_no_cond_event_when1(self): # OK
"""
n1 --> n2; h when n3[]
n3;
"""
model = ChartModel("Test")
root = model.get_root()
nn1 = root.add_simple_node("n1", 0, 0)
nn2 = root.add_simple_node("n2", 0, 0)
root.add_simple_node("n3", 0, 0)
trans = root.add_transition(nn1, nn2)
trans.set_event("h when n3")
tvisit = TableVisitor(None) # no error display
model.accept(tvisit)
reporter = ErrorRep()
cl_ds = CLDynSys(tvisit.tab_symb, reporter)
event_literal = gen_transition_clock(trans, cl_ds, None, reporter)
print("Transition clock:", str(event_literal))
assert str(event_literal) == "_lit1"
expected = [
"$not h, not n3, _lit0$",
"$not _lit0, h$",
"$not _lit0, n3$",
"$not _lit1, _lit0$",
"$not _lit1, n1$",
"$not _lit0, not n1, _lit1$",
]
assert [str(clause) for clause in cl_ds.clauses] == expected
print("free clocks registered:", cl_ds.free_clocks)
assert cl_ds.free_clocks == ["h"]
print("place_clocks", cl_ds.place_clocks)
assert cl_ds.place_clocks == {"_lit0": ["n1"]}
print("reporter: ", reporter.mess)
assert reporter.mess == ""
[docs] def test_no_cond_event_when2(self): # OK
"""
n1 --> n2; h when n3[]
n3 --> n1 ; h2 when h[]
Error h is not a state
"""
model = ChartModel("Test")
root = model.get_root()
nn1 = root.add_simple_node("n1", 0, 0)
nn2 = root.add_simple_node("n2", 0, 0)
nn3 = root.add_simple_node("n3", 0, 0)
tr1 = root.add_transition(nn1, nn2)
tr1.set_event("h when n3")
tr2 = root.add_transition(nn3, nn1)
tr2.set_event("h2 when h")
reporter = ErrorRep()
tvisit = TableVisitor(reporter) # no error display
model.accept(tvisit)
cl_ds = CLDynSys(tvisit.tab_symb, reporter)
event_literal = gen_transition_clock(tr1, cl_ds, None, reporter)
print("Transition clock:", str(event_literal))
assert str(event_literal) == "_lit1"
event_literal = gen_transition_clock(tr2, cl_ds, None, reporter)
print("Transition clock:", str(event_literal))
assert str(event_literal) == "_lit3"
expected = [
"$not h, not n3, _lit0$",
"$not _lit0, h$",
"$not _lit0, n3$",
"$not _lit1, _lit0$",
"$not _lit1, n1$",
"$not _lit0, not n1, _lit1$",
"$not h2, not h, _lit2$",
"$not _lit2, h2$",
"$not _lit2, h$",
"$not _lit3, _lit2$",
"$not _lit3, n3$",
"$not _lit2, not n3, _lit3$",
]
assert [str(clause) for clause in cl_ds.clauses] == expected
print("free clocks registered:", cl_ds.free_clocks)
assert cl_ds.free_clocks == ["h", "h2"]
print("place_clocks", cl_ds.place_clocks)
assert cl_ds.place_clocks == {"_lit2": ["n3"], "_lit0": ["n1"]}
print("reporter: ", reporter.mess)
assert "Type error: 'h' has not an expected state: 'clock'" in reporter.mess
[docs] def test_no_cond_event_when3(self): # OK
"""
n1 --> n2; h when n3[]
n3 --> n1 ; n2 when n1[]
Error n2 is not a clock
"""
model = ChartModel("Test")
root = model.get_root()
nn1 = root.add_simple_node("n1", 0, 0)
nn2 = root.add_simple_node("n2", 0, 0)
nn3 = root.add_simple_node("n3", 0, 0)
tr1 = root.add_transition(nn1, nn2)
tr1.set_event("h when n3")
tr2 = root.add_transition(nn3, nn1)
tr2.set_event("n2 when n1")
reporter = ErrorRep()
tvisit = TableVisitor(reporter) # no error display
model.accept(tvisit)
cl_ds = CLDynSys(tvisit.tab_symb, reporter)
event_literal = gen_transition_clock(tr1, cl_ds, None, reporter)
print("Transition clock:", str(event_literal))
assert str(event_literal) == "_lit1"
event_literal = gen_transition_clock(tr2, cl_ds, None, reporter)
print("Transition clock:", str(event_literal))
assert str(event_literal) == "_lit3"
expected = [
"$not h, not n3, _lit0$",
"$not _lit0, h$",
"$not _lit0, n3$",
"$not _lit1, _lit0$",
"$not _lit1, n1$",
"$not _lit0, not n1, _lit1$",
"$not _lit3, _lit2$",
"$not _lit3, n3$",
"$not _lit2, not n3, _lit3$",
]
assert [str(clause) for clause in cl_ds.clauses] == expected
print("free clocks registered:", cl_ds.free_clocks)
assert cl_ds.free_clocks == ["h"]
print("place_clocks", cl_ds.place_clocks)
assert cl_ds.place_clocks == {"_lit2": ["n3"], "_lit0": ["n1"]}
print("reporter: ", reporter.mess)
assert reporter.mess == ">> Default signal:(n2 when n1) is not a clock"
[docs] def test_no_cond_event_default(self): # OK
"""testNoCondEventWhen1
n1 --> n2; h1 when c1 default h2[c3]
"""
model = ChartModel("Test")
root = model.get_root()
nn1 = root.add_simple_node("n1", 0, 0)
nn2 = root.add_simple_node("n2", 0, 0)
root.add_simple_node("c1", 0, 0)
root.add_simple_node("c3", 0, 0)
tr1 = root.add_transition(nn1, nn2)
tr1.set_event("h when c1 default h2")
tr1.set_condition("c3")
reporter = ErrorRep()
tvisit = TableVisitor(reporter) # no error display
model.accept(tvisit)
cl_ds = CLDynSys(tvisit.tab_symb, reporter)
event_literal = gen_transition_clock(tr1, cl_ds, None, reporter)
print("Transition clock:", str(event_literal))
assert str(event_literal) == "_lit3"
expected = [
"$n1, not _lit0$",
"$c3, not _lit0$",
"$not n1, not c3, _lit0$",
"$not h, not c1, _lit2$",
"$not _lit2, h$",
"$not _lit2, c1$",
"$not _lit1, _lit2, h2$",
"$not _lit2, _lit1$",
"$not h2, _lit1$",
"$not _lit3, _lit1$",
"$not _lit3, _lit0$",
"$not _lit1, not _lit0, _lit3$",
]
assert [str(clause) for clause in cl_ds.clauses] == expected
print("free clocks registered:", cl_ds.free_clocks)
assert cl_ds.free_clocks == ["h", "h2"]
print("place_clocks", cl_ds.place_clocks)
assert cl_ds.place_clocks == {"_lit1": ["n1"]}
print("reporter: ", reporter.mess)
assert reporter.mess == ""
[docs]class TestTransitionList(unittest.TestCase):
"""
As it says
"""
[docs] def test_no_cond_on_out2events(self):
"""
n1 --> n2; h1[not n4]
n1 --> n3; h2[]
n4 --> n1; h3[]
gen_transition_list_clock tested
"""
model = ChartModel("Test")
root = model.get_root()
nn1 = root.add_simple_node("n1", 0, 0)
nn2 = root.add_simple_node("n2", 0, 0)
nn3 = root.add_simple_node("n3", 0, 0)
nn4 = root.add_simple_node("n4", 0, 0)
trans = root.add_transition(nn1, nn2)
trans.set_condition("not n4")
trans.set_event("h1")
trans = root.add_transition(nn1, nn3)
trans.set_event("h2")
trans = root.add_transition(nn4, nn1)
trans.set_event("h3")
tvisit = TableVisitor(None) # no error display/ might crash
model.accept(tvisit)
reporter = ErrorRep()
cl_ds = CLDynSys(tvisit.tab_symb, None)
trl = nn1.outgoing_trans
sed = dict()
event_literal = gen_transition_list_clock(trl, cl_ds, sed, reporter)
print("Transition clock:", str(event_literal))
assert str(event_literal) == "_lit3"
expected = [
"$n1, not _lit0$",
"$not n4, not _lit0$",
"$not n1, n4, _lit0$",
"$not _lit1, h1$",
"$not _lit1, _lit0$",
"$not h1, not _lit0, _lit1$",
"$not _lit2, h2$",
"$not _lit2, n1$",
"$not h2, not n1, _lit2$",
"$_lit3, not _lit1$",
"$_lit3, not _lit2$",
"$_lit1, _lit2, not _lit3$",
]
assert [str(clause) for clause in cl_ds.clauses] == expected
print("free clocks registered:", cl_ds.free_clocks)
assert cl_ds.free_clocks == ["h1", "h2"]
print("reporter: ", reporter.mess)
assert reporter.mess == ""
[docs] def test_very_simple(self): # OK to optimize
"""
n1 --> n2; []
"""
model = ChartModel("Test")
root = model.get_root()
nn1 = root.add_simple_node("n1", 0, 0)
nn2 = root.add_simple_node("n2", 0, 0)
root.add_transition(nn1, nn2)
model.clean_code()
tvisit = TableVisitor(None) # no error display
model.accept(tvisit)
reporter = ErrorRep()
cl_ds = CLDynSys(tvisit.tab_symb, None)
gen_simple_evolution(nn1, cl_ds, None, reporter)
expected = ["$not n1`, n1$", "$not n1`, not n1$", "$n1`, not n1, n1$"]
assert [str(clause) for clause in cl_ds.clauses] == expected
print("free clocks registered:", cl_ds.free_clocks)
assert cl_ds.free_clocks == []
model.clean_code()
print("reporter: ", reporter.mess)
assert reporter.mess == ""
[docs] def test_simple(self):
"""
n1 --> n2; h1[not n4]
n1 --> n3; h2[]
n4 --> n1; h3[]
"""
model = ChartModel("Test")
root = model.get_root()
nn1 = root.add_simple_node("n1", 0, 0)
nn2 = root.add_simple_node("n2", 0, 0)
nn3 = root.add_simple_node("n3", 0, 0)
nn4 = root.add_simple_node("n4", 0, 0)
trans = root.add_transition(nn1, nn2)
trans.set_condition("not n4")
trans.set_event("h1")
trans = root.add_transition(nn1, nn3)
trans.set_event("h2")
trans = root.add_transition(nn4, nn1)
trans.set_event("h3")
model.clean_code()
tvisit = TableVisitor(None) # no error display
model.accept(tvisit)
reporter = ErrorRep()
cl_ds = CLDynSys(tvisit.tab_symb, None)
sed = dict()
gen_simple_evolution(nn1, cl_ds, sed, reporter)
expected = [
"$not _lit0, h3$",
"$not _lit0, n4$",
"$not h3, not n4, _lit0$",
"$n1, not _lit1$",
"$not n4, not _lit1$",
"$not n1, n4, _lit1$",
"$not _lit2, h1$",
"$not _lit2, _lit1$",
"$not h1, not _lit1, _lit2$",
"$not _lit3, h2$",
"$not _lit3, n1$",
"$not h2, not n1, _lit3$",
"$_lit4, not _lit2$",
"$_lit4, not _lit3$",
"$_lit2, _lit3, not _lit4$",
"$not n1`, _lit0, n1$",
"$not n1`, _lit0, not _lit4$",
"$n1`, not _lit0$",
"$n1`, not n1, _lit4$",
]
assert [str(clause) for clause in cl_ds.clauses] == expected
print("free clocks registered:", cl_ds.free_clocks)
assert cl_ds.free_clocks == ["h3", "h1", "h2"]
model.clean_code()
print("reporter: ", reporter.mess)
assert reporter.mess == ""
[docs] def test_simple_in_no_out(self):
"""
n2 --> n1; h1[not n4]
n4 --> n1; h3[]
"""
model = ChartModel("Test")
root = model.get_root()
nn1 = root.add_simple_node("n1", 0, 0)
nn2 = root.add_simple_node("n2", 0, 0)
root.add_simple_node("n3", 0, 0)
nn4 = root.add_simple_node("n4", 0, 0)
trans = root.add_transition(nn2, nn1)
trans.set_condition("not n4")
trans.set_event("h1")
trans = root.add_transition(nn4, nn1)
trans.set_event("h3")
tvisit = TableVisitor(None) # no error display
model.accept(tvisit)
reporter = ErrorRep()
cl_ds = CLDynSys(tvisit.tab_symb, reporter)
gen_simple_evolution(nn1, cl_ds, None, reporter)
expected = [
"$n2, not _lit0$",
"$not n4, not _lit0$",
"$not n2, n4, _lit0$",
"$not _lit1, h1$",
"$not _lit1, _lit0$",
"$not h1, not _lit0, _lit1$",
"$not _lit2, h3$",
"$not _lit2, n4$",
"$not h3, not n4, _lit2$",
"$_lit3, not _lit1$",
"$_lit3, not _lit2$",
"$_lit1, _lit2, not _lit3$",
"$not n1`, _lit3, n1$",
"$n1`, not _lit3$",
"$n1`, not n1$",
]
assert [str(clause) for clause in cl_ds.clauses] == expected
print("free clocks registered:", cl_ds.free_clocks)
assert cl_ds.free_clocks == ["h1", "h3"]
print("reporter: ", reporter.mess)
assert reporter.mess == ""
[docs] def test_simple_out_no_in(self):
"""
n1 --> n2; h1[not n4]
n1 --> n3; h2[]
"""
model = ChartModel("Test")
root = model.get_root()
nn1 = root.add_simple_node("n1", 0, 0)
nn2 = root.add_simple_node("n2", 0, 0)
nn3 = root.add_simple_node("n3", 0, 0)
root.add_simple_node("n4", 0, 0)
trans = root.add_transition(nn1, nn2)
trans.set_condition("not n4")
trans.set_event("h1")
trans = root.add_transition(nn1, nn3)
trans.set_event("h2")
model.clean_code()
tvisit = TableVisitor(None) # no error display
model.accept(tvisit)
reporter = ErrorRep()
cl_ds = CLDynSys(tvisit.tab_symb, None)
gen_simple_evolution(nn1, cl_ds, None, reporter)
expected = [
"$n1, not _lit0$",
"$not n4, not _lit0$",
"$not n1, n4, _lit0$",
"$not _lit1, h1$",
"$not _lit1, _lit0$",
"$not h1, not _lit0, _lit1$",
"$not _lit2, h2$",
"$not _lit2, n1$",
"$not h2, not n1, _lit2$",
"$_lit3, not _lit1$",
"$_lit3, not _lit2$",
"$_lit1, _lit2, not _lit3$",
"$not n1`, n1$",
"$not n1`, not _lit3$",
"$n1`, not n1, _lit3$",
]
assert [str(clause) for clause in cl_ds.clauses] == expected
print("free clocks registered:", cl_ds.free_clocks)
assert cl_ds.free_clocks == ["h1", "h2"]
print("reporter: ", reporter.mess)
assert reporter.mess == ""
[docs] def test_simple_no_trans(self): # OK
"""
n1;
"""
model = ChartModel("Test")
root = model.get_root()
nn1 = root.add_simple_node("n1", 0, 0)
tvisit = TableVisitor(None) # no error display
model.accept(tvisit)
reporter = ErrorRep()
cl_ds = CLDynSys(tvisit.tab_symb, None)
gen_simple_evolution(nn1, cl_ds, None, reporter)
expected = ["$not n1`, n1$", "$n1`, not n1$"]
assert [str(clause) for clause in cl_ds.clauses] == expected
print("free clocks registered:", cl_ds.free_clocks)
assert cl_ds.free_clocks == []
print("reporter: ", reporter.mess)
assert reporter.mess == ""
[docs]class TestFull(unittest.TestCase):
"""
test full models
"""
[docs] def test_model1(self):
"""
n1 --> n2; h1[not n4]
n1 --> n3; h2[]
n4 --> n1; h3[]
"""
model = ChartModel("Test")
root = model.get_root()
nn1 = root.add_simple_node("n1", 0, 0)
nn2 = root.add_simple_node("n2", 0, 0)
nn3 = root.add_simple_node("n3", 0, 0)
nn4 = root.add_simple_node("n4", 0, 0)
trans = root.add_transition(nn1, nn2)
trans.set_condition("not n4")
trans.set_event("h1")
trans = root.add_transition(nn1, nn3)
trans.set_event("h2")
trans = root.add_transition(nn4, nn1)
trans.set_event("h3")
tvisit = TableVisitor(None) # no error display
model.accept(tvisit)
reporter = ErrorRep()
cl_ds = CLDynSys(tvisit.tab_symb, reporter)
gt2clauses = GT2Clauses(cl_ds, False, reporter)
model.accept(gt2clauses)
expected = [
"$not _lit0, h3$",
"$not _lit0, n4$",
"$not h3, not n4, _lit0$",
"$n1, not _lit1$",
"$not n4, not _lit1$",
"$not n1, n4, _lit1$",
"$not _lit2, h1$",
"$not _lit2, _lit1$",
"$not h1, not _lit1, _lit2$",
"$not _lit3, h2$",
"$not _lit3, n1$",
"$not h2, not n1, _lit3$",
"$_lit4, not _lit2$",
"$_lit4, not _lit3$",
"$_lit2, _lit3, not _lit4$",
"$not n1`, _lit0, n1$",
"$not n1`, _lit0, not _lit4$",
"$n1`, not _lit0$",
"$n1`, not n1, _lit4$",
"$not n2`, _lit2, n2$",
"$n2`, not _lit2$",
"$n2`, not n2$",
"$not n3`, _lit3, n3$",
"$n3`, not _lit3$",
"$n3`, not n3$",
"$not n4`, n4$",
"$not n4`, not _lit0$",
"$n4`, not n4, _lit0$",
]
assert [str(clause) for clause in cl_ds.clauses] == expected
print("variables:", cl_ds.base_var_set)
print("free clocks registered:", cl_ds.free_clocks)
print("place_clocks:", cl_ds.place_clocks)
print("inputs:", cl_ds.inputs)
expected = {
"n3", "h2", "h3", "h1", "_lit2", "_lit3", "n1", "_lit1", "_lit0",
"n4", "n2", "_lit4",
}
assert cl_ds.base_var_set == expected
assert cl_ds.free_clocks == ["h3", "h1", "h2"]
assert cl_ds.place_clocks == {"h2": ["n1"], "h3": ["n4"], "h1": ["n1"]}
assert cl_ds.inputs == []
[docs] def test_model2(self): # OK
"""
n1 --> n2; h1 when n2 default h2[not n4]
n1 --> n3; h2 when n4[]
n4 --> n1; h3[]
"""
model = ChartModel("Test")
root = model.get_root()
nn1 = root.add_simple_node("n1", 0, 0)
nn2 = root.add_simple_node("n2", 0, 0)
nn3 = root.add_simple_node("n3", 0, 0)
nn4 = root.add_simple_node("n4", 0, 0)
trans = root.add_transition(nn1, nn2)
trans.set_condition("not n4")
trans.set_event("h1 when n2 default h2")
trans = root.add_transition(nn1, nn3)
trans.set_event("h2 when n4")
trans = root.add_transition(nn4, nn1)
trans.set_event("h3")
tvisit = TableVisitor(None) # no error display
model.accept(tvisit)
reporter = ErrorRep()
cl_ds = CLDynSys(tvisit.tab_symb, reporter)
gt2clauses = GT2Clauses(cl_ds, reporter, False)
model.accept(gt2clauses)
expected = [
"$not _lit0, h3$",
"$not _lit0, n4$",
"$not h3, not n4, _lit0$",
"$n1, not _lit1$",
"$not n4, not _lit1$",
"$not n1, n4, _lit1$",
"$not h1, not n2, _lit3$",
"$not _lit3, h1$",
"$not _lit3, n2$",
"$not _lit2, _lit3, h2$",
"$not _lit3, _lit2$",
"$not h2, _lit2$",
"$not _lit4, _lit2$",
"$not _lit4, _lit1$",
"$not _lit2, not _lit1, _lit4$",
"$not h2, not n4, _lit5$",
"$not _lit5, h2$",
"$not _lit5, n4$",
"$not _lit6, _lit5$",
"$not _lit6, n1$",
"$not _lit5, not n1, _lit6$",
"$_lit7, not _lit4$",
"$_lit7, not _lit6$",
"$_lit4, _lit6, not _lit7$",
"$not n1`, _lit0, n1$",
"$not n1`, _lit0, not _lit7$",
"$n1`, not _lit0$",
"$n1`, not n1, _lit7$",
"$not n2`, _lit4, n2$",
"$n2`, not _lit4$",
"$n2`, not n2$",
"$not n3`, _lit6, n3$",
"$n3`, not _lit6$",
"$n3`, not n3$",
"$not n4`, n4$",
"$not n4`, not _lit0$",
"$n4`, not n4, _lit0$",
]
assert [str(clause) for clause in cl_ds.clauses] == expected
print("variables:", cl_ds.base_var_set)
print("free clocks registered:", cl_ds.free_clocks)
print("place_clocks:", cl_ds.place_clocks)
print("inputs:", cl_ds.inputs)
expected = {
"n3", "h2", "h3", "h1", "_lit6", "_lit7", "_lit2", "_lit3", "n1",
"_lit1", "_lit0", "n4", "n2", "_lit5", "_lit4",
}
assert cl_ds.base_var_set == expected
assert cl_ds.free_clocks == ["h3", "h1", "h2"]
assert cl_ds.place_clocks == {"h3": ["n4"], "_lit5": ["n1"], "_lit2": ["n1"]}
assert cl_ds.inputs == []
[docs] def test_model3(self): # OK
"""testInputCondEvent
n4;
n1/p --> n2; h[n4];
"""
model = ChartModel("Test")
root = model.get_root()
nn1 = root.add_perm_node("n1", 0, 0)
nn2 = root.add_simple_node("n2", 0, 0)
root.add_simple_node("n4", 0, 0)
trans = root.add_transition(nn1, nn2)
trans.set_condition("n4")
trans.set_event("h")
tvisit = TableVisitor(None) # no error display
model.accept(tvisit)
reporter = ErrorRep()
cl_ds = CLDynSys(tvisit.tab_symb, None)
tvisit = TableVisitor(None) # no error display
model.accept(tvisit)
reporter = ErrorRep()
cl_ds = CLDynSys(tvisit.tab_symb, reporter)
gt2clauses = GT2Clauses(cl_ds, reporter, False)
model.accept(gt2clauses)
expected = [
"$not _lit0, h$",
"$not _lit0, n4$",
"$not h, not n4, _lit0$",
"$not n2`, _lit0, n2$",
"$n2`, not _lit0$",
"$n2`, not n2$",
"$not n4`, n4$",
"$n4`, not n4$",
]
assert [str(clause) for clause in cl_ds.clauses] == expected
print("variables:", cl_ds.base_var_set)
print("free clocks registered:", cl_ds.free_clocks)
print("place_clocks:", cl_ds.place_clocks)
print("inputs:", cl_ds.inputs)
expected = {"h", "n2", "_lit0", "n4"}
assert cl_ds.base_var_set == expected
assert cl_ds.free_clocks == ["h"]
assert cl_ds.place_clocks == {}
assert cl_ds.inputs == []
[docs] def test_constraints(self):
"""
As it says
"""
model = ChartModel("Test")
root = model.get_root()
aaa = root.add_simple_node("A", 0, 0)
bbb = root.add_simple_node("B", 0, 0)
ccc = root.add_simple_node("C", 0, 0)
ddd = root.add_simple_node("D", 0, 0)
trans = root.add_transition(aaa, bbb)
trans.set_event("h1 default h2")
trans = root.add_transition(ccc, ddd)
trans.set_event("h3")
cont = "synchro(h1, h3);exclus(h1, h2);included(h3, h2);"
model.constraints = cont
tvisit = TableVisitor(None) # no error display
model.accept(tvisit)
reporter = ErrorRep()
cl_ds = CLDynSys(tvisit.tab_symb, reporter)
gt2clauses = GT2Clauses(cl_ds, reporter, False)
model.accept(gt2clauses)
expected = [
"$not _lit0, h1, h2$",
"$not h1, _lit0$",
"$not h2, _lit0$",
"$not _lit1, _lit0$",
"$not _lit1, A$",
"$not _lit0, not A, _lit1$",
"$not A`, A$",
"$not A`, not _lit1$",
"$A`, not A, _lit1$",
"$not B`, _lit1, B$",
"$B`, not _lit1$",
"$B`, not B$",
"$not _lit2, h3$",
"$not _lit2, C$",
"$not h3, not C, _lit2$",
"$not C`, C$",
"$not C`, not _lit2$",
"$C`, not C, _lit2$",
"$not D`, _lit2, D$",
"$D`, not _lit2$",
"$D`, not D$",
"$not h1, h3$",
"$h1, not h3$",
"$not h1, not h2$",
"$not h3, h2$",
]
assert [str(clause) for clause in cl_ds.clauses] == expected
print("variables:", cl_ds.base_var_set)
print("free clocks registered:", cl_ds.free_clocks)
print("place_clocks:", cl_ds.place_clocks)
print("inputs:", cl_ds.inputs)
expected = {"A", "C", "B", "D", "h2", "h3", "h1", "_lit2", "_lit1", "_lit0"}
assert cl_ds.base_var_set == expected
assert cl_ds.free_clocks == ["h1", "h2", "h3"]
assert cl_ds.place_clocks == {"h3": ["C"], "_lit0": ["A"]}
assert cl_ds.inputs == []
[docs] def test_antlr_optimization(self):
"""Optimization gain comparison when using MCLTranslator optimizations
for ANTLR translation (subexpression elimination)
.. note:: Use test file instead of not provided:
"../ucl/examples/test_tgfb_ref_300511.bcx"
"""
rep = ErrorRep()
mcla = MCLAnalyser(rep)
mcla.translator_opti = False
filename = pkg_resources.resource_filename(
__name__, # package name
"../../guard_transitions/translators/tests/tgf_cano_noclock_cmp.cal",
)
mcla.build_from_cadlang(filename)
nb_clauses_without_opti = len(mcla.dynamic_system.clauses)
print("NB Clauses without opti:", nb_clauses_without_opti)
mcla = MCLAnalyser(rep)
filename = pkg_resources.resource_filename(
__name__, # package name
"../../guard_transitions/translators/tests/tgf_cano_noclock_cmp.cal",
)
mcla.build_from_cadlang(filename)
nb_clauses_with_opti = len(mcla.dynamic_system.clauses)
print("NB Clauses with opti:", nb_clauses_with_opti)
assert nb_clauses_with_opti < nb_clauses_without_opti
assert nb_clauses_with_opti == 1573
assert nb_clauses_without_opti == 1909
[docs]class TestMCLSigExprVisitor(unittest.TestCase):
"""
Test of signal expression
"""
[docs] def test_ident1(self):
"""
sigexp = xx
"""
sexpr = SigIdentExpr("xx")
cl_ds = CLDynSys(None, None)
sexpv = MCLSigExprVisitor(cl_ds, "Y", None)
# Formula
assert str(sexpr) == "xx"
var = sexpr.accept(sexpv)
# Return aux var
assert str(var) == "xx"
# Clauses
assert [str(clause) for clause in cl_ds.clauses] == []
[docs] def test_bin1(self):
"""
X or Y
"""
sexpr1 = SigIdentExpr("x")
sexpr2 = SigIdentExpr("y")
sexpr = SigSyncBinExpr("or", sexpr1, sexpr2)
# Formula
assert str(sexpr) == "(x or y)"
cl_ds = CLDynSys(None, None)
sexpv = MCLSigExprVisitor(cl_ds, "Z", dict())
var = sexpr.accept(sexpv)
# Return aux var
assert str(var) == "Z"
# Clauses
expected = ["$not x, Z$", "$not y, Z$", "$x, y, not Z$"]
assert [str(clause) for clause in cl_ds.clauses] == expected
[docs] def test_bin2(self):
"""
X and Y
"""
sexpr1 = SigIdentExpr("x")
sexpr2 = SigIdentExpr("y")
sexpr = SigSyncBinExpr("and", sexpr1, sexpr2)
# Formula
assert str(sexpr) == "(x and y)"
cl_ds = CLDynSys(None, None)
sexpv = MCLSigExprVisitor(cl_ds, "Z", dict())
sexpv.output_lit = None # for output var generation
var = sexpr.accept(sexpv)
# Return aux var
assert str(var) == "_lit0"
# Clauses
expected = ["$x, not _lit0$", "$y, not _lit0$", "$not x, not y, _lit0$"]
assert [str(clause) for clause in cl_ds.clauses] == expected
[docs] def test_bin3(self):
"""
h1 default h2
"""
sexpr1 = SigIdentExpr("h1")
sexpr2 = SigIdentExpr("h2")
sexpr = SigDefaultExpr(sexpr1, sexpr2)
# Formula
assert str(sexpr) == "(h1 default h2)"
symb_tab = dict()
symb_tab["h1"] = ("clock", -1)
symb_tab["h2"] = ("clock", -1)
cl_ds = CLDynSys(symb_tab, None)
sexpv = MCLSigExprVisitor(cl_ds, None)
# sexpv.output_lit = None # for output var generation
var = sexpr.accept(sexpv)
# Return aux var
assert str(var) == "_lit0"
# Clauses
expected = ["$not _lit0, h1, h2$", "$not h1, _lit0$", "$not h2, _lit0$"]
assert [str(clause) for clause in cl_ds.clauses] == expected
[docs] def test_bin4(self):
"""
h1 when (a or b)
"""
sexpr1 = SigIdentExpr("h1")
sexpr3 = SigIdentExpr("a")
sexpr4 = SigIdentExpr("b")
sexpr = SigSyncBinExpr("or", sexpr3, sexpr4)
sexpr = SigWhenExpr(sexpr1, sexpr)
# Formula
assert str(sexpr) == "(h1 when (a or b))"
symb_tab = dict()
symb_tab["h1"] = ("clock", -1)
cl_ds = CLDynSys(symb_tab, None)
sexpv = MCLSigExprVisitor(cl_ds, None)
# sexpv.output_lit = None # for output var generation
var = sexpr.accept(sexpv)
# Return aux var
assert str(var) == "_lit0"
# Clauses
expected = [
"$not a, _lit1$",
"$not b, _lit1$",
"$a, b, not _lit1$",
"$not h1, not _lit1, _lit0$",
"$not _lit0, h1$",
"$not _lit0, _lit1$",
]
assert [str(clause) for clause in cl_ds.clauses] == expected
[docs] def test_cse1(self):
"""
common subexpression elimination
h1 when (a or b) default h2 when (b or a)
"""
sexpr1 = SigIdentExpr("h1")
sexpr2 = SigIdentExpr("h2")
sexpr3 = SigIdentExpr("a")
sexpr4 = SigIdentExpr("b")
a_or_b1 = SigSyncBinExpr("and", sexpr3, sexpr4)
a_or_b2 = SigSyncBinExpr("and", sexpr4, sexpr3)
hh1 = SigWhenExpr(sexpr1, a_or_b1)
hh2 = SigWhenExpr(sexpr2, a_or_b2)
sexpr = SigDefaultExpr(hh1, hh2)
# Formula
assert str(sexpr) == "((h1 when (a and b)) default (h2 when (b and a)))"
symb_tab = dict()
symb_tab["h1"] = ("clock", -1)
symb_tab["h2"] = ("clock", -1)
cl_ds = CLDynSys(symb_tab, None)
sub_exp = dict()
sexpv = MCLSigExprVisitor(cl_ds, None, sub_exp)
# sexpv.output_lit = None # for output var generation
var = sexpr.accept(sexpv)
# Return aux var
assert str(var) == "_lit0"
# Clauses
expected = [
"$a, not _lit2$",
"$b, not _lit2$",
"$not a, not b, _lit2$",
"$not h1, not _lit2, _lit1$",
"$not _lit1, h1$",
"$not _lit1, _lit2$",
"$not h2, not _lit2, _lit3$",
"$not _lit3, h2$",
"$not _lit3, _lit2$",
"$not _lit0, _lit1, _lit3$",
"$not _lit1, _lit0$",
"$not _lit3, _lit0$",
]
assert [str(clause) for clause in cl_ds.clauses] == expected
[docs] def test_cse2(self):
"""
common subexpression elimination
h1 when (a or b) default h2 when (b or a)
"""
hh1 = SigIdentExpr("h1")
hh2 = SigIdentExpr("h2")
h12 = SigDefaultExpr(hh1, hh2)
h21 = SigDefaultExpr(hh2, hh1)
sexpr = SigDefaultExpr(h12, h21)
# Formula
assert str(sexpr) == "((h1 default h2) default (h2 default h1))"
symb_tab = dict()
symb_tab["h1"] = ("clock", -1)
symb_tab["h2"] = ("clock", -1)
cl_ds = CLDynSys(symb_tab, None)
sub_exp = dict()
sexpv = MCLSigExprVisitor(cl_ds, None, sub_exp)
# sexpv.output_lit = None # for output var generation
var = sexpr.accept(sexpv)
# Return aux var
assert str(var) == "_lit0"
# Clauses
expected = [
"$not _lit1, h1, h2$",
"$not h1, _lit1$",
"$not h2, _lit1$",
"$not _lit0, _lit1, _lit1$",
"$not _lit1, _lit0$",
"$not _lit1, _lit0$",
]
assert [str(clause) for clause in cl_ds.clauses] == expected