TestMCLTranslators.py 43.1 KB
Newer Older
1
# -*- coding: utf-8 -*-
VIGNET Pierre's avatar
VIGNET Pierre committed
2
3
4
## Filename    : TestMCLTranslators.py
## Author(s)   : Michel Le Borgne
## Created     : 9 mars 2012
5
6
## Revision    :
## Source      :
VIGNET Pierre's avatar
VIGNET Pierre committed
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
##
## Copyright 2012 : 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
37
##     35042 RENNES Cedex, FRANCE
VIGNET Pierre's avatar
VIGNET Pierre committed
38
##
39
40
##
## Contributor(s):
VIGNET Pierre's avatar
VIGNET Pierre committed
41
42
43
44
##
"""
Unitary tests for the translators
"""
45
from __future__ import print_function
46
import pkg_resources
VIGNET Pierre's avatar
VIGNET Pierre committed
47
48
import unittest

49
from cadbiom.models.clause_constraints.CLDynSys import CLDynSys
50
51
52
53
54
55
56
57
58
59
60
61
62
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,
)
63
64
65
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
VIGNET Pierre's avatar
VIGNET Pierre committed
66
67
68
69
70
71
72


# simple reporter
class ErrorRep(object):
    """
    Simple error reporter
    """
73

VIGNET Pierre's avatar
VIGNET Pierre committed
74
75
76
77
    def __init__(self):
        self.mess = ""
        self.error = False
        pass
78

VIGNET Pierre's avatar
VIGNET Pierre committed
79
80
81
82
83
    def display(self, mess):
        """
        set error and print
        """
        self.error = True
84
85
        self.mess += ">> " + mess
        print(" DISPLAY CALL>> " + mess)
VIGNET Pierre's avatar
VIGNET Pierre committed
86
87
88
89
90
91


class TestTransitionClauses(unittest.TestCase):
    """
    Test of transitions into clauses
    """
92

93
    def test_no_cond(self):  # OK
VIGNET Pierre's avatar
VIGNET Pierre committed
94
95
96
97
98
        """
        n1 --> n2; []
        """
        model = ChartModel("Test")
        root = model.get_root()
99
100
        nn1 = root.add_simple_node("n1", 0, 0)
        nn2 = root.add_simple_node("n2", 0, 0)
VIGNET Pierre's avatar
VIGNET Pierre committed
101
        trans = root.add_transition(nn1, nn2)
102

103
        tvisit = TableVisitor(None)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
104
105
106
        model.accept(tvisit)
        reporter = ErrorRep()
        cl_ds = CLDynSys(tvisit, reporter)
107
108
109
110
111
112
113
114
115
116
117
118
119

        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 == ""

    def test_cond(self):  # OK
VIGNET Pierre's avatar
VIGNET Pierre committed
120
121
122
123
124
        """
        n1 --> n2; [not n3]
        """
        model = ChartModel("Test")
        root = model.get_root()
125
126
127
        nn1 = root.add_simple_node("n1", 0, 0)
        nn2 = root.add_simple_node("n2", 0, 0)
        root.add_simple_node("n3", 0, 0)
VIGNET Pierre's avatar
VIGNET Pierre committed
128
129
        trans = root.add_transition(nn1, nn2)
        trans.set_condition("not n3")
130

131
        tvisit = TableVisitor(None)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
132
133
        model.accept(tvisit)
        reporter = ErrorRep()
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
        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 == ""

    def test_no_cond_event(self):  # OK
VIGNET Pierre's avatar
VIGNET Pierre committed
150
151
152
153
154
        """
        n1 --> n2; h[]
        """
        model = ChartModel("Test")
        root = model.get_root()
155
156
        nn1 = root.add_simple_node("n1", 0, 0)
        nn2 = root.add_simple_node("n2", 0, 0)
VIGNET Pierre's avatar
VIGNET Pierre committed
157
        trans = root.add_transition(nn1, nn2)
158
        trans.set_event("h")
159

160
        tvisit = TableVisitor(None)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
161
162
163
        model.accept(tvisit)
        reporter = ErrorRep()
        cl_ds = CLDynSys(tvisit.tab_symb, reporter)
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178

        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 ----------------")
VIGNET Pierre's avatar
VIGNET Pierre committed
179
        sed = dict()
180
        tvisit = TableVisitor(None)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
181
182
        model.accept(tvisit)
        cl_ds = CLDynSys(tvisit.tab_symb, reporter)
183
184
185
186
187
188
189
190
191
192
193
        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 == ""
194

195
    def test_cond_event(self):  # OK
VIGNET Pierre's avatar
VIGNET Pierre committed
196
197
198
199
200
        """
        n1 --> n2; h[not n3]
        """
        model = ChartModel("Test")
        root = model.get_root()
201
202
203
        nn1 = root.add_simple_node("n1", 0, 0)
        nn2 = root.add_simple_node("n2", 0, 0)
        root.add_simple_node("n3", 0, 0)
VIGNET Pierre's avatar
VIGNET Pierre committed
204
205
        trans = root.add_transition(nn1, nn2)
        trans.set_condition("not n3")
206
        trans.set_event("h")
207

208
        tvisit = TableVisitor(None)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
209
210
        model.accept(tvisit)
        reporter = ErrorRep()
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
        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 ----------------")
VIGNET Pierre's avatar
VIGNET Pierre committed
234
        sed = dict()
235
        tvisit = TableVisitor(None)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
236
237
        model.accept(tvisit)
        reporter = ErrorRep()
238
        cl_ds = CLDynSys(tvisit.tab_symb, None)
239

240
241
242
        event_literal = gen_transition_clock(trans, cl_ds, sed, reporter)
        print("Transition clock:", str(event_literal))
        assert str(event_literal) == "_lit1"
243

244
        assert [str(clause) for clause in cl_ds.clauses] == expected
245

246
247
        print("free clocks registered:", cl_ds.free_clocks)
        assert cl_ds.free_clocks == ["h"]
248

249
250
        print("reporter: ", reporter.mess)
        assert reporter.mess == ""
251

252
    def test_perm_no_cond_event(self):  # OK
VIGNET Pierre's avatar
VIGNET Pierre committed
253
254
255
256
257
        """
        n1/p --> n2; h[];
        """
        model = ChartModel("Test")
        root = model.get_root()
258
259
        nn1 = root.add_perm_node("n1", 0, 0)
        nn2 = root.add_simple_node("n2", 0, 0)
VIGNET Pierre's avatar
VIGNET Pierre committed
260
        trans = root.add_transition(nn1, nn2)
261
        trans.set_event("h")
262

263
        tvisit = TableVisitor(None)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
264
265
        model.accept(tvisit)
        reporter = ErrorRep()
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
        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 == ""

    def test_perm_cond_event(self):  # OK
VIGNET Pierre's avatar
VIGNET Pierre committed
282
283
284
285
286
287
        """
        n4;
        n1/p --> n2; h[n4];
        """
        model = ChartModel("Test")
        root = model.get_root()
288
289
290
        nn1 = root.add_perm_node("n1", 0, 0)
        nn2 = root.add_simple_node("n2", 0, 0)
        root.add_simple_node("n4", 0, 0)
VIGNET Pierre's avatar
VIGNET Pierre committed
291
292
        trans = root.add_transition(nn1, nn2)
        trans.set_condition("n4")
293
        trans.set_event("h")
294

295
        tvisit = TableVisitor(None)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
296
297
        model.accept(tvisit)
        reporter = ErrorRep()
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
        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 == ""

    def test_input_cond_event(self):  # OK
VIGNET Pierre's avatar
VIGNET Pierre committed
314
315
316
317
318
319
        """
        n4/i;
        n1/i --> n2; h[n4];
        """
        model = ChartModel("Test")
        root = model.get_root()
320
321
322
        nn1 = root.add_input_node("n1", 0, 0)
        nn2 = root.add_simple_node("n2", 0, 0)
        root.add_input_node("n4", 0, 0)
VIGNET Pierre's avatar
VIGNET Pierre committed
323
324
        trans = root.add_transition(nn1, nn2)
        trans.set_condition("n4")
325
        trans.set_event("h")
326

327
        tvisit = TableVisitor(None)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
328
329
        model.accept(tvisit)
        reporter = ErrorRep()
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
        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$",
            "$n4, not _lit0$",
            "$not n1, not n4, _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 == ""
351

VIGNET Pierre's avatar
VIGNET Pierre committed
352
    # complex events
353
    def test_no_cond_event_when1(self):  # OK
VIGNET Pierre's avatar
VIGNET Pierre committed
354
355
356
357
358
359
        """
        n1 --> n2; h when n3[]
        n3;
        """
        model = ChartModel("Test")
        root = model.get_root()
360
361
362
        nn1 = root.add_simple_node("n1", 0, 0)
        nn2 = root.add_simple_node("n2", 0, 0)
        root.add_simple_node("n3", 0, 0)
VIGNET Pierre's avatar
VIGNET Pierre committed
363
        trans = root.add_transition(nn1, nn2)
364
        trans.set_event("h when n3")
365

366
        tvisit = TableVisitor(None)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
367
368
369
        model.accept(tvisit)
        reporter = ErrorRep()
        cl_ds = CLDynSys(tvisit.tab_symb, reporter)
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394

        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 == ""

    def test_no_cond_event_when2(self):  # OK
VIGNET Pierre's avatar
VIGNET Pierre committed
395
396
397
398
399
400
401
        """
        n1 --> n2; h when n3[]
        n3 --> n1 ; h2 when h[]
        Error h is not a state
        """
        model = ChartModel("Test")
        root = model.get_root()
402
403
404
        nn1 = root.add_simple_node("n1", 0, 0)
        nn2 = root.add_simple_node("n2", 0, 0)
        nn3 = root.add_simple_node("n3", 0, 0)
VIGNET Pierre's avatar
VIGNET Pierre committed
405
        tr1 = root.add_transition(nn1, nn2)
406
        tr1.set_event("h when n3")
VIGNET Pierre's avatar
VIGNET Pierre committed
407
        tr2 = root.add_transition(nn3, nn1)
408
        tr2.set_event("h2 when h")
409

VIGNET Pierre's avatar
VIGNET Pierre committed
410
        reporter = ErrorRep()
411
        tvisit = TableVisitor(reporter)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
412
        model.accept(tvisit)
413

VIGNET Pierre's avatar
VIGNET Pierre committed
414
        cl_ds = CLDynSys(tvisit.tab_symb, reporter)
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449

        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"]}

        # TODO: check this
        print("reporter: ", reporter.mess)
        assert reporter.mess == ">> type error -> h is not a state (clock)"

    def test_no_cond_event_when3(self):  # OK
VIGNET Pierre's avatar
VIGNET Pierre committed
450
451
452
453
454
455
456
        """
        n1 --> n2; h when n3[]
        n3 --> n1 ; n2 when n1[]
        Error n2 is not a clock
        """
        model = ChartModel("Test")
        root = model.get_root()
457
458
459
        nn1 = root.add_simple_node("n1", 0, 0)
        nn2 = root.add_simple_node("n2", 0, 0)
        nn3 = root.add_simple_node("n3", 0, 0)
VIGNET Pierre's avatar
VIGNET Pierre committed
460
        tr1 = root.add_transition(nn1, nn2)
461
        tr1.set_event("h when n3")
VIGNET Pierre's avatar
VIGNET Pierre committed
462
        tr2 = root.add_transition(nn3, nn1)
463
        tr2.set_event("n2 when n1")
464

VIGNET Pierre's avatar
VIGNET Pierre committed
465
        reporter = ErrorRep()
466
        tvisit = TableVisitor(reporter)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
467
        model.accept(tvisit)
468

VIGNET Pierre's avatar
VIGNET Pierre committed
469
        cl_ds = CLDynSys(tvisit.tab_symb, reporter)
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502

        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"]}

        # TODO: check this
        print("reporter: ", reporter.mess)
        assert reporter.mess == ">> Default signal:(n2 when n1) is not a clock"

    def test_no_cond_event_default(self):  # OK
        """testNoCondEventWhen1
VIGNET Pierre's avatar
VIGNET Pierre committed
503
504
505
506
        n1 --> n2; h1 when c1 default h2[c3]
        """
        model = ChartModel("Test")
        root = model.get_root()
507
508
509
510
        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)
VIGNET Pierre's avatar
VIGNET Pierre committed
511
        tr1 = root.add_transition(nn1, nn2)
512
513
        tr1.set_event("h when c1 default h2")
        tr1.set_condition("c3")
514

VIGNET Pierre's avatar
VIGNET Pierre committed
515
        reporter = ErrorRep()
516
        tvisit = TableVisitor(reporter)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
517
        model.accept(tvisit)
518

VIGNET Pierre's avatar
VIGNET Pierre committed
519
520
        cl_ds = CLDynSys(tvisit.tab_symb, reporter)

521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
        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 == ""
549
550


VIGNET Pierre's avatar
VIGNET Pierre committed
551
552
553
class TestTransitionList(unittest.TestCase):
    """
    As it says
554
555
    """

VIGNET Pierre's avatar
VIGNET Pierre committed
556
557
558
559
560
561
562
563
564
    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()
565
566
567
568
        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)
VIGNET Pierre's avatar
VIGNET Pierre committed
569
570
        trans = root.add_transition(nn1, nn2)
        trans.set_condition("not n4")
571
        trans.set_event("h1")
VIGNET Pierre's avatar
VIGNET Pierre committed
572
        trans = root.add_transition(nn1, nn3)
573
        trans.set_event("h2")
VIGNET Pierre's avatar
VIGNET Pierre committed
574
        trans = root.add_transition(nn4, nn1)
575
        trans.set_event("h3")
576

577
        tvisit = TableVisitor(None)  # no error display/ might crash
VIGNET Pierre's avatar
VIGNET Pierre committed
578
        model.accept(tvisit)
579

VIGNET Pierre's avatar
VIGNET Pierre committed
580
        reporter = ErrorRep()
581
        cl_ds = CLDynSys(tvisit.tab_symb, None)
VIGNET Pierre's avatar
VIGNET Pierre committed
582
583
        trl = nn1.outgoing_trans
        sed = dict()
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
        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 == ""

    def test_very_simple(self):  # OK to optimize
VIGNET Pierre's avatar
VIGNET Pierre committed
611
612
613
614
615
        """
        n1 --> n2; []
        """
        model = ChartModel("Test")
        root = model.get_root()
616
617
618
        nn1 = root.add_simple_node("n1", 0, 0)
        nn2 = root.add_simple_node("n2", 0, 0)
        root.add_transition(nn1, nn2)
619

VIGNET Pierre's avatar
VIGNET Pierre committed
620
        model.clean_code()
621
        tvisit = TableVisitor(None)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
622
623
        model.accept(tvisit)
        reporter = ErrorRep()
624
625
        cl_ds = CLDynSys(tvisit.tab_symb, None)

626
        gen_simple_evolution(nn1, cl_ds, None, reporter)
627
628
629
630
631
632
633

        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 == []

VIGNET Pierre's avatar
VIGNET Pierre committed
634
        model.clean_code()
635

636
637
638
        print("reporter: ", reporter.mess)
        assert reporter.mess == ""

VIGNET Pierre's avatar
VIGNET Pierre committed
639
640
641
642
643
644
645
646
    def test_simple(self):
        """
        n1 --> n2; h1[not n4]
        n1 --> n3; h2[]
        n4 --> n1; h3[]
        """
        model = ChartModel("Test")
        root = model.get_root()
647
648
649
650
        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)
VIGNET Pierre's avatar
VIGNET Pierre committed
651
652
        trans = root.add_transition(nn1, nn2)
        trans.set_condition("not n4")
653
        trans.set_event("h1")
VIGNET Pierre's avatar
VIGNET Pierre committed
654
        trans = root.add_transition(nn1, nn3)
655
        trans.set_event("h2")
VIGNET Pierre's avatar
VIGNET Pierre committed
656
        trans = root.add_transition(nn4, nn1)
657
        trans.set_event("h3")
658

VIGNET Pierre's avatar
VIGNET Pierre committed
659
        model.clean_code()
660
        tvisit = TableVisitor(None)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
661
662
        model.accept(tvisit)
        reporter = ErrorRep()
663
664
        cl_ds = CLDynSys(tvisit.tab_symb, None)

VIGNET Pierre's avatar
VIGNET Pierre committed
665
        sed = dict()
666
        gen_simple_evolution(nn1, cl_ds, sed, reporter)
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693

        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"]

VIGNET Pierre's avatar
VIGNET Pierre committed
694
695
        model.clean_code()

696
697
698
        print("reporter: ", reporter.mess)
        assert reporter.mess == ""

VIGNET Pierre's avatar
VIGNET Pierre committed
699
700
701
702
703
704
705
    def test_simple_in_no_out(self):
        """
        n2 --> n1; h1[not n4]
        n4 --> n1; h3[]
        """
        model = ChartModel("Test")
        root = model.get_root()
706
707
708
709
        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)
VIGNET Pierre's avatar
VIGNET Pierre committed
710
711
        trans = root.add_transition(nn2, nn1)
        trans.set_condition("not n4")
712
        trans.set_event("h1")
VIGNET Pierre's avatar
VIGNET Pierre committed
713
        trans = root.add_transition(nn4, nn1)
714
        trans.set_event("h3")
715

716
        tvisit = TableVisitor(None)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
717
718
        model.accept(tvisit)
        reporter = ErrorRep()
719
720
        cl_ds = CLDynSys(tvisit.tab_symb, reporter)

721
        gen_simple_evolution(nn1, cl_ds, None, reporter)
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746

        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 == ""
747

VIGNET Pierre's avatar
VIGNET Pierre committed
748
749
750
751
752
753
754
    def test_simple_out_no_in(self):
        """
        n1 --> n2; h1[not n4]
        n1 --> n3; h2[]
        """
        model = ChartModel("Test")
        root = model.get_root()
755
756
757
758
        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)
VIGNET Pierre's avatar
VIGNET Pierre committed
759
760
        trans = root.add_transition(nn1, nn2)
        trans.set_condition("not n4")
761
        trans.set_event("h1")
VIGNET Pierre's avatar
VIGNET Pierre committed
762
        trans = root.add_transition(nn1, nn3)
763
        trans.set_event("h2")
764

VIGNET Pierre's avatar
VIGNET Pierre committed
765
        model.clean_code()
766
        tvisit = TableVisitor(None)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
767
768
        model.accept(tvisit)
        reporter = ErrorRep()
769
770
        cl_ds = CLDynSys(tvisit.tab_symb, None)

771
772
        gen_simple_evolution(nn1, cl_ds, None, reporter)

773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
        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 == ""

    def test_simple_no_trans(self):  # OK
VIGNET Pierre's avatar
VIGNET Pierre committed
799
800
801
802
803
        """
        n1;
        """
        model = ChartModel("Test")
        root = model.get_root()
804
        nn1 = root.add_simple_node("n1", 0, 0)
VIGNET Pierre's avatar
VIGNET Pierre committed
805

806
        tvisit = TableVisitor(None)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
807
808
        model.accept(tvisit)
        reporter = ErrorRep()
809
810
        cl_ds = CLDynSys(tvisit.tab_symb, None)

811
        gen_simple_evolution(nn1, cl_ds, None, reporter)
812
813
814
815
816
817
818
819
820

        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 == ""
821
822


VIGNET Pierre's avatar
VIGNET Pierre committed
823
824
825
826
class TestFull(unittest.TestCase):
    """
    test full models
    """
827

VIGNET Pierre's avatar
VIGNET Pierre committed
828
829
830
831
832
833
834
835
    def test_model1(self):
        """
        n1 --> n2; h1[not n4]
        n1 --> n3; h2[]
        n4 --> n1; h3[]
        """
        model = ChartModel("Test")
        root = model.get_root()
836
837
838
839
        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)
VIGNET Pierre's avatar
VIGNET Pierre committed
840
841
        trans = root.add_transition(nn1, nn2)
        trans.set_condition("not n4")
842
        trans.set_event("h1")
VIGNET Pierre's avatar
VIGNET Pierre committed
843
        trans = root.add_transition(nn1, nn3)
844
        trans.set_event("h2")
VIGNET Pierre's avatar
VIGNET Pierre committed
845
        trans = root.add_transition(nn4, nn1)
846
        trans.set_event("h3")
847

848
        tvisit = TableVisitor(None)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
849
850
        model.accept(tvisit)
        reporter = ErrorRep()
851
852
        cl_ds = CLDynSys(tvisit.tab_symb, reporter)

VIGNET Pierre's avatar
VIGNET Pierre committed
853
        gt2clauses = GT2Clauses(cl_ds, False, reporter)
854
        model.accept(gt2clauses)
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
        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 == []

    def test_model2(self):  # OK
VIGNET Pierre's avatar
VIGNET Pierre committed
912
913
914
915
916
917
918
        """
        n1 --> n2; h1 when n2 default h2[not n4]
        n1 --> n3; h2 when n4[]
        n4 --> n1; h3[]
        """
        model = ChartModel("Test")
        root = model.get_root()
919
920
921
922
        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)
VIGNET Pierre's avatar
VIGNET Pierre committed
923
924
        trans = root.add_transition(nn1, nn2)
        trans.set_condition("not n4")
925
        trans.set_event("h1 when n2 default h2")
VIGNET Pierre's avatar
VIGNET Pierre committed
926
        trans = root.add_transition(nn1, nn3)
927
        trans.set_event("h2 when n4")
VIGNET Pierre's avatar
VIGNET Pierre committed
928
        trans = root.add_transition(nn4, nn1)
929
        trans.set_event("h3")
930

931
        tvisit = TableVisitor(None)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
932
933
        model.accept(tvisit)
        reporter = ErrorRep()
934
935
        cl_ds = CLDynSys(tvisit.tab_symb, reporter)

VIGNET Pierre's avatar
VIGNET Pierre committed
936
        gt2clauses = GT2Clauses(cl_ds, reporter, False)
937
938
        model.accept(gt2clauses)

939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
        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 == []

    def test_model3(self):  # OK
        """testInputCondEvent
VIGNET Pierre's avatar
VIGNET Pierre committed
1009
1010
1011
1012
1013
        n4;
        n1/p --> n2; h[n4];
        """
        model = ChartModel("Test")
        root = model.get_root()
1014
1015
1016
        nn1 = root.add_perm_node("n1", 0, 0)
        nn2 = root.add_simple_node("n2", 0, 0)
        root.add_simple_node("n4", 0, 0)
VIGNET Pierre's avatar
VIGNET Pierre committed
1017
1018
        trans = root.add_transition(nn1, nn2)
        trans.set_condition("n4")
1019
        trans.set_event("h")
1020

1021
        tvisit = TableVisitor(None)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
1022
1023
        model.accept(tvisit)
        reporter = ErrorRep()
1024
        cl_ds = CLDynSys(tvisit.tab_symb, None)
1025

1026
        tvisit = TableVisitor(None)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
1027
1028
        model.accept(tvisit)
        reporter = ErrorRep()
1029
1030
        cl_ds = CLDynSys(tvisit.tab_symb, reporter)

VIGNET Pierre's avatar
VIGNET Pierre committed
1031
        gt2clauses = GT2Clauses(cl_ds, reporter, False)
1032
1033
        model.accept(gt2clauses)

1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
        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 == []
1056

VIGNET Pierre's avatar
VIGNET Pierre committed
1057
1058
1059
1060
1061
1062
    def test_constraints(self):
        """
        As it says
        """
        model = ChartModel("Test")
        root = model.get_root()
1063
1064
1065
1066
        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)
VIGNET Pierre's avatar
VIGNET Pierre committed
1067
        trans = root.add_transition(aaa, bbb)
1068
        trans.set_event("h1 default h2")
VIGNET Pierre's avatar
VIGNET Pierre committed
1069
        trans = root.add_transition(ccc, ddd)
1070
1071
        trans.set_event("h3")
        cont = "synchro(h1, h3);exclus(h1, h2);included(h3, h2);"
VIGNET Pierre's avatar
VIGNET Pierre committed
1072
        model.constraints = cont
1073
        tvisit = TableVisitor(None)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
1074
1075
        model.accept(tvisit)
        reporter = ErrorRep()
1076
        cl_ds = CLDynSys(tvisit.tab_symb, reporter)
VIGNET Pierre's avatar
VIGNET Pierre committed
1077
        gt2clauses = GT2Clauses(cl_ds, reporter, False)
1078
        model.accept(gt2clauses)
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118

        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 == []
1119

1120
1121
1122
1123
1124
1125
    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"
1126
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
1127
        rep = ErrorRep()
1128

VIGNET Pierre's avatar
VIGNET Pierre committed
1129
        mcla = MCLAnalyser(rep)
1130
1131
        mcla.translator_opti = False
        filename = pkg_resources.resource_filename(
1132
1133
            __name__,  # package name
            "../../guard_transitions/translators/tests/tgf_cano_noclock_cmp.cal",
1134
1135
        )
        mcla.build_from_cadlang(filename)
1136
        nb_clauses_without_opti = len(mcla.dynamic_system.clauses)
1137
        print("NB Clauses without opti:", nb_clauses_without_opti)
1138

VIGNET Pierre's avatar
VIGNET Pierre committed
1139
        mcla = MCLAnalyser(rep)
1140
        filename = pkg_resources.resource_filename(
1141
1142
            __name__,  # package name
            "../../guard_transitions/translators/tests/tgf_cano_noclock_cmp.cal",
1143
1144
        )
        mcla.build_from_cadlang(filename)
1145
        nb_clauses_with_opti = len(mcla.dynamic_system.clauses)
1146
        print("NB Clauses with opti:", nb_clauses_with_opti)
1147
1148
1149
1150

        assert nb_clauses_with_opti < nb_clauses_without_opti
        assert nb_clauses_with_opti == 1573
        assert nb_clauses_without_opti == 1909
1151

1152
1153

class TestMCLSigExprVisitor(unittest.TestCase):
VIGNET Pierre's avatar
VIGNET Pierre committed
1154
1155
1156
    """
    Test of signal expression
    """
1157

VIGNET Pierre's avatar
VIGNET Pierre committed
1158
1159
1160
1161
    def test_ident1(self):
        """
        sigexp = xx
        """
1162
        sexpr = SigIdentExpr("xx")
VIGNET Pierre's avatar
VIGNET Pierre committed
1163
        cl_ds = CLDynSys(None, None)
1164
1165
1166
1167
1168
        sexpv = MCLSigExprVisitor(cl_ds, "Y", None)

        # Formula
        assert str(sexpr) == "xx"

VIGNET Pierre's avatar
VIGNET Pierre committed
1169
        var = sexpr.accept(sexpv)
1170
1171
1172
1173
1174

        # Return aux var
        assert str(var) == "xx"
        # Clauses
        assert [str(clause) for clause in cl_ds.clauses] == []
1175

VIGNET Pierre's avatar
VIGNET Pierre committed
1176
1177
1178
1179
    def test_bin1(self):
        """
        X or Y
        """
1180
1181
1182
1183
1184
1185
1186
        sexpr1 = SigIdentExpr("x")
        sexpr2 = SigIdentExpr("y")
        sexpr = SigSyncBinExpr("or", sexpr1, sexpr2)

        # Formula
        assert str(sexpr) == "(x or y)"

VIGNET Pierre's avatar
VIGNET Pierre committed
1187
        cl_ds = CLDynSys(None, None)
1188
        sexpv = MCLSigExprVisitor(cl_ds, "Z", dict())
VIGNET Pierre's avatar
VIGNET Pierre committed
1189
        var = sexpr.accept(sexpv)
1190
1191
1192
1193
1194
1195

        # 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
1196

VIGNET Pierre's avatar
VIGNET Pierre committed
1197
1198
1199
1200
    def test_bin2(self):
        """
        X and Y
        """
1201
1202
1203
1204
1205
1206
1207
        sexpr1 = SigIdentExpr("x")
        sexpr2 = SigIdentExpr("y")
        sexpr = SigSyncBinExpr("and", sexpr1, sexpr2)

        # Formula
        assert str(sexpr) == "(x and y)"

VIGNET Pierre's avatar
VIGNET Pierre committed
1208
        cl_ds = CLDynSys(None, None)
1209
1210
        sexpv = MCLSigExprVisitor(cl_ds, "Z", dict())
        sexpv.output_lit = None  # for output var generation
VIGNET Pierre's avatar
VIGNET Pierre committed
1211
        var = sexpr.accept(sexpv)
1212
1213
1214
1215
1216
1217

        # 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
1218

VIGNET Pierre's avatar
VIGNET Pierre committed
1219
1220
    def test_bin3(self):
        """
1221
        h1 default h2
VIGNET Pierre's avatar
VIGNET Pierre committed
1222
        """
1223
1224
        sexpr1 = SigIdentExpr("h1")
        sexpr2 = SigIdentExpr("h2")
VIGNET Pierre's avatar
VIGNET Pierre committed
1225
        sexpr = SigDefaultExpr(sexpr1, sexpr2)
1226
1227
1228
1229

        # Formula
        assert str(sexpr) == "(h1 default h2)"

VIGNET Pierre's avatar
VIGNET Pierre committed
1230
        symb_tab = dict()
1231
1232
        symb_tab["h1"] = ("clock", -1)
        symb_tab["h2"] = ("clock", -1)
VIGNET Pierre's avatar
VIGNET Pierre committed
1233
1234
        cl_ds = CLDynSys(symb_tab, None)
        sexpv = MCLSigExprVisitor(cl_ds, None)
1235
        # sexpv.output_lit = None # for output var generation
VIGNET Pierre's avatar
VIGNET Pierre committed
1236
        var = sexpr.accept(sexpv)
1237
1238
1239
1240
1241
1242

        # 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
1243

VIGNET Pierre's avatar
VIGNET Pierre committed
1244
1245
    def test_bin4(self):
        """
1246
        h1 when (a or b)
VIGNET Pierre's avatar
VIGNET Pierre committed
1247
        """