Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

TestMCLTranslators.py 42.7 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


class ErrorRep(object):
69
    """Simple error reporter"""
70

VIGNET Pierre's avatar
VIGNET Pierre committed
71
72
73
    def __init__(self):
        self.mess = ""
        self.error = False
74

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


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

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

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

        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
116
117
118
119
120
        """
        n1 --> n2; [not n3]
        """
        model = ChartModel("Test")
        root = model.get_root()
121
122
123
        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
124
125
        trans = root.add_transition(nn1, nn2)
        trans.set_condition("not n3")
126

127
        tvisit = TableVisitor(None)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
128
129
        model.accept(tvisit)
        reporter = ErrorRep()
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
        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
146
147
148
149
150
        """
        n1 --> n2; h[]
        """
        model = ChartModel("Test")
        root = model.get_root()
151
152
        nn1 = root.add_simple_node("n1", 0, 0)
        nn2 = root.add_simple_node("n2", 0, 0)
VIGNET Pierre's avatar
VIGNET Pierre committed
153
        trans = root.add_transition(nn1, nn2)
154
        trans.set_event("h")
155

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

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

191
    def test_cond_event(self):  # OK
VIGNET Pierre's avatar
VIGNET Pierre committed
192
193
194
195
196
        """
        n1 --> n2; h[not n3]
        """
        model = ChartModel("Test")
        root = model.get_root()
197
198
199
        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
200
201
        trans = root.add_transition(nn1, nn2)
        trans.set_condition("not n3")
202
        trans.set_event("h")
203

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

236
237
238
        event_literal = gen_transition_clock(trans, cl_ds, sed, reporter)
        print("Transition clock:", str(event_literal))
        assert str(event_literal) == "_lit1"
239

240
        assert [str(clause) for clause in cl_ds.clauses] == expected
241

242
243
        print("free clocks registered:", cl_ds.free_clocks)
        assert cl_ds.free_clocks == ["h"]
244

245
246
        print("reporter: ", reporter.mess)
        assert reporter.mess == ""
247

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

259
        tvisit = TableVisitor(None)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
260
261
        model.accept(tvisit)
        reporter = ErrorRep()
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
        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
278
279
280
281
282
283
        """
        n4;
        n1/p --> n2; h[n4];
        """
        model = ChartModel("Test")
        root = model.get_root()
284
285
286
        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
287
288
        trans = root.add_transition(nn1, nn2)
        trans.set_condition("n4")
289
        trans.set_event("h")
290

291
        tvisit = TableVisitor(None)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
292
293
        model.accept(tvisit)
        reporter = ErrorRep()
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
        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
310
311
312
313
314
315
        """
        n4/i;
        n1/i --> n2; h[n4];
        """
        model = ChartModel("Test")
        root = model.get_root()
316
317
318
        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
319
320
        trans = root.add_transition(nn1, nn2)
        trans.set_condition("n4")
321
        trans.set_event("h")
322

323
        tvisit = TableVisitor(None)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
324
325
        model.accept(tvisit)
        reporter = ErrorRep()
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
        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 == ""
347

VIGNET Pierre's avatar
VIGNET Pierre committed
348
    # complex events
349
    def test_no_cond_event_when1(self):  # OK
VIGNET Pierre's avatar
VIGNET Pierre committed
350
351
352
353
354
355
        """
        n1 --> n2; h when n3[]
        n3;
        """
        model = ChartModel("Test")
        root = model.get_root()
356
357
358
        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
359
        trans = root.add_transition(nn1, nn2)
360
        trans.set_event("h when n3")
361

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

        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
391
392
393
394
395
396
397
        """
        n1 --> n2; h when n3[]
        n3 --> n1 ; h2 when h[]
        Error h is not a state
        """
        model = ChartModel("Test")
        root = model.get_root()
398
399
400
        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
401
        tr1 = root.add_transition(nn1, nn2)
402
        tr1.set_event("h when n3")
VIGNET Pierre's avatar
VIGNET Pierre committed
403
        tr2 = root.add_transition(nn3, nn1)
404
        tr2.set_event("h2 when h")
405

VIGNET Pierre's avatar
VIGNET Pierre committed
406
        reporter = ErrorRep()
407
        tvisit = TableVisitor(reporter)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
408
        model.accept(tvisit)
409

VIGNET Pierre's avatar
VIGNET Pierre committed
410
        cl_ds = CLDynSys(tvisit.tab_symb, reporter)
411
412
413
414
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

        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 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
445
446
447
448
449
450
451
        """
        n1 --> n2; h when n3[]
        n3 --> n1 ; n2 when n1[]
        Error n2 is not a clock
        """
        model = ChartModel("Test")
        root = model.get_root()
452
453
454
        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
455
        tr1 = root.add_transition(nn1, nn2)
456
        tr1.set_event("h when n3")
VIGNET Pierre's avatar
VIGNET Pierre committed
457
        tr2 = root.add_transition(nn3, nn1)
458
        tr2.set_event("n2 when n1")
459

VIGNET Pierre's avatar
VIGNET Pierre committed
460
        reporter = ErrorRep()
461
        tvisit = TableVisitor(reporter)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
462
        model.accept(tvisit)
463

VIGNET Pierre's avatar
VIGNET Pierre committed
464
        cl_ds = CLDynSys(tvisit.tab_symb, reporter)
465
466
467
468
469
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

        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"

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

VIGNET Pierre's avatar
VIGNET Pierre committed
509
        reporter = ErrorRep()
510
        tvisit = TableVisitor(reporter)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
511
        model.accept(tvisit)
512

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

515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
        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 == ""
543
544


VIGNET Pierre's avatar
VIGNET Pierre committed
545
546
547
class TestTransitionList(unittest.TestCase):
    """
    As it says
548
549
    """

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

571
        tvisit = TableVisitor(None)  # no error display/ might crash
VIGNET Pierre's avatar
VIGNET Pierre committed
572
        model.accept(tvisit)
573

VIGNET Pierre's avatar
VIGNET Pierre committed
574
        reporter = ErrorRep()
575
        cl_ds = CLDynSys(tvisit.tab_symb, None)
VIGNET Pierre's avatar
VIGNET Pierre committed
576
577
        trl = nn1.outgoing_trans
        sed = dict()
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
        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
605
606
607
608
609
        """
        n1 --> n2; []
        """
        model = ChartModel("Test")
        root = model.get_root()
610
611
612
        nn1 = root.add_simple_node("n1", 0, 0)
        nn2 = root.add_simple_node("n2", 0, 0)
        root.add_transition(nn1, nn2)
613

VIGNET Pierre's avatar
VIGNET Pierre committed
614
        model.clean_code()
615
        tvisit = TableVisitor(None)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
616
617
        model.accept(tvisit)
        reporter = ErrorRep()
618
619
        cl_ds = CLDynSys(tvisit.tab_symb, None)

620
        gen_simple_evolution(nn1, cl_ds, None, reporter)
621
622
623
624
625
626
627

        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
628
        model.clean_code()
629

630
631
632
        print("reporter: ", reporter.mess)
        assert reporter.mess == ""

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

VIGNET Pierre's avatar
VIGNET Pierre committed
653
        model.clean_code()
654
        tvisit = TableVisitor(None)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
655
656
        model.accept(tvisit)
        reporter = ErrorRep()
657
658
        cl_ds = CLDynSys(tvisit.tab_symb, None)

VIGNET Pierre's avatar
VIGNET Pierre committed
659
        sed = dict()
660
        gen_simple_evolution(nn1, cl_ds, sed, reporter)
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687

        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
688
689
        model.clean_code()

690
691
692
        print("reporter: ", reporter.mess)
        assert reporter.mess == ""

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

710
        tvisit = TableVisitor(None)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
711
712
        model.accept(tvisit)
        reporter = ErrorRep()
713
714
        cl_ds = CLDynSys(tvisit.tab_symb, reporter)

715
        gen_simple_evolution(nn1, cl_ds, None, reporter)
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740

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

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

VIGNET Pierre's avatar
VIGNET Pierre committed
759
        model.clean_code()
760
        tvisit = TableVisitor(None)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
761
762
        model.accept(tvisit)
        reporter = ErrorRep()
763
764
        cl_ds = CLDynSys(tvisit.tab_symb, None)

765
766
        gen_simple_evolution(nn1, cl_ds, None, reporter)

767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
        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
793
794
795
796
797
        """
        n1;
        """
        model = ChartModel("Test")
        root = model.get_root()
798
        nn1 = root.add_simple_node("n1", 0, 0)
VIGNET Pierre's avatar
VIGNET Pierre committed
799

800
        tvisit = TableVisitor(None)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
801
802
        model.accept(tvisit)
        reporter = ErrorRep()
803
804
        cl_ds = CLDynSys(tvisit.tab_symb, None)

805
        gen_simple_evolution(nn1, cl_ds, None, reporter)
806
807
808
809
810
811
812
813
814

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


VIGNET Pierre's avatar
VIGNET Pierre committed
817
818
819
820
class TestFull(unittest.TestCase):
    """
    test full models
    """
821

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

842
        tvisit = TableVisitor(None)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
843
844
        model.accept(tvisit)
        reporter = ErrorRep()
845
846
        cl_ds = CLDynSys(tvisit.tab_symb, reporter)

VIGNET Pierre's avatar
VIGNET Pierre committed
847
        gt2clauses = GT2Clauses(cl_ds, False, reporter)
848
        model.accept(gt2clauses)
849
850
851
852
853
854
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
        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 = {
887
888
            "n3", "h2", "h3", "h1", "_lit2", "_lit3", "n1", "_lit1", "_lit0",
            "n4", "n2", "_lit4",
889
890
891
892
893
894
895
        }
        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
896
897
898
899
900
901
902
        """
        n1 --> n2; h1 when n2 default h2[not n4]
        n1 --> n3; h2 when n4[]
        n4 --> n1; h3[]
        """
        model = ChartModel("Test")
        root = model.get_root()
903
904
905
906
        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
907
908
        trans = root.add_transition(nn1, nn2)
        trans.set_condition("not n4")
909
        trans.set_event("h1 when n2 default h2")
VIGNET Pierre's avatar
VIGNET Pierre committed
910
        trans = root.add_transition(nn1, nn3)
911
        trans.set_event("h2 when n4")
VIGNET Pierre's avatar
VIGNET Pierre committed
912
        trans = root.add_transition(nn4, nn1)
913
        trans.set_event("h3")
914

915
        tvisit = TableVisitor(None)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
916
917
        model.accept(tvisit)
        reporter = ErrorRep()
918
919
        cl_ds = CLDynSys(tvisit.tab_symb, reporter)

VIGNET Pierre's avatar
VIGNET Pierre committed
920
        gt2clauses = GT2Clauses(cl_ds, reporter, False)
921
922
        model.accept(gt2clauses)

923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
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
        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 = {
970
971
            "n3", "h2", "h3", "h1", "_lit6", "_lit7", "_lit2", "_lit3", "n1",
            "_lit1", "_lit0", "n4", "n2", "_lit5", "_lit4",
972
973
974
975
976
977
978
979
        }
        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
980
981
982
983
984
        n4;
        n1/p --> n2; h[n4];
        """
        model = ChartModel("Test")
        root = model.get_root()
985
986
987
        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
988
989
        trans = root.add_transition(nn1, nn2)
        trans.set_condition("n4")
990
        trans.set_event("h")
991

992
        tvisit = TableVisitor(None)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
993
994
        model.accept(tvisit)
        reporter = ErrorRep()
995
        cl_ds = CLDynSys(tvisit.tab_symb, None)
996

997
        tvisit = TableVisitor(None)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
998
999
        model.accept(tvisit)
        reporter = ErrorRep()
1000
1001
        cl_ds = CLDynSys(tvisit.tab_symb, reporter)

VIGNET Pierre's avatar
VIGNET Pierre committed
1002
        gt2clauses = GT2Clauses(cl_ds, reporter, False)
1003
1004
        model.accept(gt2clauses)

1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
        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 == []
1027

VIGNET Pierre's avatar
VIGNET Pierre committed
1028
1029
1030
1031
1032
1033
    def test_constraints(self):
        """
        As it says
        """
        model = ChartModel("Test")
        root = model.get_root()
1034
1035
1036
1037
        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
1038
        trans = root.add_transition(aaa, bbb)
1039
        trans.set_event("h1 default h2")
VIGNET Pierre's avatar
VIGNET Pierre committed
1040
        trans = root.add_transition(ccc, ddd)
1041
1042
        trans.set_event("h3")
        cont = "synchro(h1, h3);exclus(h1, h2);included(h3, h2);"
VIGNET Pierre's avatar
VIGNET Pierre committed
1043
        model.constraints = cont
1044
        tvisit = TableVisitor(None)  # no error display
VIGNET Pierre's avatar
VIGNET Pierre committed
1045
1046
        model.accept(tvisit)
        reporter = ErrorRep()
1047
        cl_ds = CLDynSys(tvisit.tab_symb, reporter)
VIGNET Pierre's avatar
VIGNET Pierre committed
1048
        gt2clauses = GT2Clauses(cl_ds, reporter, False)
1049
        model.accept(gt2clauses)
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089

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

1091
1092
1093
1094
1095
1096
    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"
1097
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
1098
        rep = ErrorRep()
1099

VIGNET Pierre's avatar
VIGNET Pierre committed
1100
        mcla = MCLAnalyser(rep)
1101
1102
        mcla.translator_opti = False
        filename = pkg_resources.resource_filename(
1103
1104
            __name__,  # package name
            "../../guard_transitions/translators/tests/tgf_cano_noclock_cmp.cal",
1105
1106
        )
        mcla.build_from_cadlang(filename)
1107
        nb_clauses_without_opti = len(mcla.dynamic_system.clauses)
1108
        print("NB Clauses without opti:", nb_clauses_without_opti)
1109

VIGNET Pierre's avatar
VIGNET Pierre committed
1110
        mcla = MCLAnalyser(rep)
1111
        filename = pkg_resources.resource_filename(
1112
1113
            __name__,  # package name
            "../../guard_transitions/translators/tests/tgf_cano_noclock_cmp.cal",
1114
1115
        )
        mcla.build_from_cadlang(filename)
1116
        nb_clauses_with_opti = len(mcla.dynamic_system.clauses)
1117
        print("NB Clauses with opti:", nb_clauses_with_opti)
1118
1119
1120
1121

        assert nb_clauses_with_opti < nb_clauses_without_opti
        assert nb_clauses_with_opti == 1573
        assert nb_clauses_without_opti == 1909
1122

1123
1124

class TestMCLSigExprVisitor(unittest.TestCase):
VIGNET Pierre's avatar
VIGNET Pierre committed
1125
1126
1127
    """
    Test of signal expression
    """
1128

VIGNET Pierre's avatar
VIGNET Pierre committed
1129
1130
1131
1132
    def test_ident1(self):
        """
        sigexp = xx
        """
1133
        sexpr = SigIdentExpr("xx")
VIGNET Pierre's avatar
VIGNET Pierre committed
1134
        cl_ds = CLDynSys(None, None)
1135
1136
1137
1138
1139
        sexpv = MCLSigExprVisitor(cl_ds, "Y", None)

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

VIGNET Pierre's avatar
VIGNET Pierre committed
1140
        var = sexpr.accept(sexpv)
1141
1142
1143
1144
1145

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

VIGNET Pierre's avatar
VIGNET Pierre committed
1147
1148
1149
1150
    def test_bin1(self):
        """
        X or Y
        """
1151
1152
1153
1154
1155
1156
1157
        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
1158
        cl_ds = CLDynSys(None, None)
1159
        sexpv = MCLSigExprVisitor(cl_ds, "Z", dict())
VIGNET Pierre's avatar
VIGNET Pierre committed
1160
        var = sexpr.accept(sexpv)
1161
1162
1163
1164
1165
1166

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

VIGNET Pierre's avatar
VIGNET Pierre committed
1168
1169
1170
1171
    def test_bin2(self):
        """
        X and Y
        """
1172
1173
1174
1175
1176
1177
1178
        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
1179
        cl_ds = CLDynSys(None, None)
1180
1181
        sexpv = MCLSigExprVisitor(cl_ds, "Z", dict())
        sexpv.output_lit = None  # for output var generation
VIGNET Pierre's avatar
VIGNET Pierre committed
1182
        var = sexpr.accept(sexpv)
1183
1184
1185
1186
1187
1188

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

VIGNET Pierre's avatar
VIGNET Pierre committed
1190
1191
    def test_bin3(self):
        """
1192
        h1 default h2
VIGNET Pierre's avatar
VIGNET Pierre committed
1193
        """
1194
1195
        sexpr1 = SigIdentExpr("h1")
        sexpr2 = SigIdentExpr("h2")
VIGNET Pierre's avatar
VIGNET Pierre committed
1196
        sexpr = SigDefaultExpr(sexpr1, sexpr2)
1197
1198
1199
1200

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

VIGNET Pierre's avatar
VIGNET Pierre committed
1201
        symb_tab = dict()
1202
1203
        symb_tab["h1"] = ("clock", -1)
        symb_tab["h2"] = ("clock", -1)
VIGNET Pierre's avatar
VIGNET Pierre committed
1204
1205
        cl_ds = CLDynSys(symb_tab, None)
        sexpv = MCLSigExprVisitor(cl_ds, None)
1206
        # sexpv.output_lit = None # for output var generation
VIGNET Pierre's avatar
VIGNET Pierre committed
1207
        var = sexpr.accept(sexpv)
1208
1209
1210
1211
1212
1213

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

VIGNET Pierre's avatar
VIGNET Pierre committed
1215
1216
    def test_bin4(self):
        """
1217
        h1 when (a or b)
VIGNET Pierre's avatar
VIGNET Pierre committed
1218
        """
1219
1220
1221
1222
        sexpr1 = SigIdentExpr("h1")
        sexpr3 = SigIdentExpr("a")
        sexpr4 = SigIdentExpr("b")
        sexpr = SigSyncBinExpr("or", sexpr3, sexpr4)
VIGNET Pierre's avatar
VIGNET Pierre committed
1223
        sexpr = SigWhenExpr(sexpr1, sexpr)
1224
1225
1226
1227

        # Formula
        assert str(sexpr) == "(h1 when (a or b))"

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

        # Return aux var
        assert str(var) == "_lit0"
        # Clauses