TestMCLTranslators.py 35.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
49
import unittest
import sys

50
51
from cadbiom.models.clause_constraints.CLDynSys import CLDynSys
from cadbiom.models.clause_constraints.mcl.MCLTranslators import  MCLSigExprVisitor, \
VIGNET Pierre's avatar
VIGNET Pierre committed
52
53
            gen_transition_clock, gen_transition_list_clock, \
            gen_simple_evolution, GT2Clauses
54
from cadbiom.models.biosignal.sig_expr import SigIdentExpr, \
VIGNET Pierre's avatar
VIGNET Pierre committed
55
            SigSyncBinExpr, SigWhenExpr, SigDefaultExpr
56
57
58
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
59
60
61
62
63
64
65
66
67
68
69


# simple reporter
class ErrorRep(object):
    """
    Simple error reporter
    """
    def __init__(self):
        self.mess = ""
        self.error = False
        pass
70

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

TRACE_FILE = sys.stdout
#TRACE_FILE = open("/tmp/testMCLTranslator.txt",'w')

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

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

VIGNET Pierre's avatar
VIGNET Pierre committed
97
98
99
100
101
102
103
104
        tvisit = TableVisitor(None) # no error display
        model.accept(tvisit)
        reporter = ErrorRep()
        cl_ds = CLDynSys(tvisit, reporter)
        TRACE_FILE.write('\ntestNoCond')
        TRACE_FILE.write( '\n\nn1 --> n2; []\n')
        htr = gen_transition_clock(trans, cl_ds, None, reporter)
        TRACE_FILE.write( 'Transition clock:'+ htr.__str__()+'\n')
105
        for cla in cl_ds.clauses:
VIGNET Pierre's avatar
VIGNET Pierre committed
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
            TRACE_FILE.write( cla.__str__()+'\n')
        mess = 'free clocks registered:' + cl_ds.free_clocks.__str__() + '\n'
        TRACE_FILE.write(mess)
        TRACE_FILE.write( 'reporter: '+ reporter.mess+'\n')

    def test_cond(self): #OK
        """
        n1 --> n2; [not n3]
        """
        model = ChartModel("Test")
        root = model.get_root()
        nn1 = root.add_simple_node('n1', 0, 0)
        nn2 = root.add_simple_node('n2', 0, 0)
        nn3 = root.add_simple_node('n3', 0, 0)
        trans = root.add_transition(nn1, nn2)
        trans.set_condition("not n3")
122

VIGNET Pierre's avatar
VIGNET Pierre committed
123
124
125
126
127
128
129
130
        tvisit = TableVisitor(None) # no error display
        model.accept(tvisit)
        reporter = ErrorRep()
        cl_ds = CLDynSys( tvisit.tab_symb, None)
        TRACE_FILE.write('\ntestCond')
        TRACE_FILE.write( '\n\nn1 --> n2; [not n3]'+'\n')
        htr = gen_transition_clock(trans, cl_ds, None, reporter)
        TRACE_FILE.write( 'Transition clock:' + htr.__str__()+'\n')
131
        for cla in cl_ds.clauses:
VIGNET Pierre's avatar
VIGNET Pierre committed
132
133
134
135
            TRACE_FILE.write( cla.__str__() + '\n')
        mess =  'free clocks registered:' + cl_ds.free_clocks.__str__()+'\n'
        TRACE_FILE.write(mess)
        TRACE_FILE.write( 'reporter: '+ reporter.mess+'\n')
136

VIGNET Pierre's avatar
VIGNET Pierre committed
137
138
139
140
141
142
143
144
145
146
    def test_no_cond_event(self): #OK
        """
        n1 --> n2; h[]
        """
        model = ChartModel("Test")
        root = model.get_root()
        nn1 = root.add_simple_node('n1', 0, 0)
        nn2 = root.add_simple_node('n2', 0, 0)
        trans = root.add_transition(nn1, nn2)
        trans.set_event('h')
147

VIGNET Pierre's avatar
VIGNET Pierre committed
148
149
150
151
152
        tvisit = TableVisitor(None) # no error display
        model.accept(tvisit)
        reporter = ErrorRep()
        cl_ds = CLDynSys(tvisit.tab_symb, reporter)
        TRACE_FILE.write('\ntestNoCondEvent')
153
        TRACE_FILE.write( '\n\nn1 --> n2; h[]'+'\n')
VIGNET Pierre's avatar
VIGNET Pierre committed
154
155
        htr = gen_transition_clock(trans, cl_ds, None, reporter)
        TRACE_FILE.write( 'Transition clock:'+ htr.__str__()+'\n')
156
        for cla in cl_ds.clauses:
VIGNET Pierre's avatar
VIGNET Pierre committed
157
158
159
160
            TRACE_FILE.write( cla.__str__() + '\n')
        mess = 'free clocks registered:' +cl_ds.free_clocks.__str__()+'\n'
        TRACE_FILE.write(mess)
        TRACE_FILE.write( 'reporter: '+ reporter.mess+'\n')
161

VIGNET Pierre's avatar
VIGNET Pierre committed
162
163
164
165
166
167
168
        TRACE_FILE.write( '---------- opti ----------------\n')
        sed = dict()
        tvisit = TableVisitor(None) # no error display
        model.accept(tvisit)
        cl_ds = CLDynSys(tvisit.tab_symb, reporter)
        htr = gen_transition_clock(trans, cl_ds, sed, reporter)
        TRACE_FILE.write( 'Transition clock:'+ htr.__str__()+'\n')
169
        for cla in cl_ds.clauses:
VIGNET Pierre's avatar
VIGNET Pierre committed
170
171
172
173
            TRACE_FILE.write( cla.__str__()+'\n')
        mess = 'free clocks registered:' + cl_ds.free_clocks.__str__() + '\n'
        TRACE_FILE.write(mess)
        TRACE_FILE.write( 'reporter: '+ reporter.mess+'\n')
174

VIGNET Pierre's avatar
VIGNET Pierre committed
175
176
177
178
179
180
181
182
183
184
185
186
    def test_cond_event(self): #OK
        """
        n1 --> n2; h[not n3]
        """
        model = ChartModel("Test")
        root = model.get_root()
        nn1 = root.add_simple_node('n1', 0, 0)
        nn2 = root.add_simple_node('n2', 0, 0)
        nn3 = root.add_simple_node('n3', 0, 0)
        trans = root.add_transition(nn1, nn2)
        trans.set_condition("not n3")
        trans.set_event('h')
187

VIGNET Pierre's avatar
VIGNET Pierre committed
188
189
190
191
192
        tvisit = TableVisitor(None) # no error display
        model.accept(tvisit)
        reporter = ErrorRep()
        cl_ds = CLDynSys( tvisit.tab_symb, None)
        TRACE_FILE.write('\ntestCondEvent')
193
        TRACE_FILE.write( '\n\nn1 --> n2; h[not n3]'+'\n')
VIGNET Pierre's avatar
VIGNET Pierre committed
194
195
        htr = gen_transition_clock(trans, cl_ds, None, reporter)
        TRACE_FILE.write( 'Transition clock:'+ htr.__str__()+'\n')
196
        for cla in cl_ds.clauses:
VIGNET Pierre's avatar
VIGNET Pierre committed
197
198
199
200
            TRACE_FILE.write( cla.__str__()+'\n')
        mess = 'free clocks registered:'+ cl_ds.free_clocks.__str__()+'\n'
        TRACE_FILE.write(mess)
        TRACE_FILE.write( 'reporter: '+ reporter.mess+'\n')
201

VIGNET Pierre's avatar
VIGNET Pierre committed
202
203
204
205
206
207
208
        TRACE_FILE.write( '---------- opti ----------------\n')
        sed = dict()
        tvisit = TableVisitor(None) # no error display
        model.accept(tvisit)
        reporter = ErrorRep()
        cl_ds = CLDynSys( tvisit.tab_symb, None)
        TRACE_FILE.write('\ntestCondEvent')
209
        TRACE_FILE.write( '\n\nn1 --> n2; h[not n3]'+'\n')
VIGNET Pierre's avatar
VIGNET Pierre committed
210
211
        htr = gen_transition_clock(trans, cl_ds, sed, reporter)
        TRACE_FILE.write( 'Transition clock:'+ htr.__str__()+'\n')
212
        for cla in cl_ds.clauses:
VIGNET Pierre's avatar
VIGNET Pierre committed
213
214
215
            TRACE_FILE.write( cla.__str__()+'\n')
        mess = 'free clocks registered:'+ cl_ds.free_clocks.__str__()+'\n'
        TRACE_FILE.write(mess)
216
217
218
219
220
221
        TRACE_FILE.write( 'reporter: '+ reporter.mess+'\n')





VIGNET Pierre's avatar
VIGNET Pierre committed
222
223
224
225
226
227
228
229
230
231
    def test_perm_no_cond_event(self): #OK
        """
        n1/p --> n2; h[];
        """
        model = ChartModel("Test")
        root = model.get_root()
        nn1 = root.add_perm_node('n1', 0, 0)
        nn2 = root.add_simple_node('n2', 0, 0)
        trans = root.add_transition(nn1, nn2)
        trans.set_event('h')
232

VIGNET Pierre's avatar
VIGNET Pierre committed
233
234
235
236
237
238
239
240
        tvisit = TableVisitor(None) # no error display
        model.accept(tvisit)
        reporter = ErrorRep()
        cl_ds = CLDynSys( tvisit.tab_symb, None)
        TRACE_FILE.write('\ntestPermNoCondEvent')
        TRACE_FILE.write( '\n\nn1/p --> n2; h[]'+'\n' )
        htr = gen_transition_clock(trans, cl_ds, None, reporter)
        TRACE_FILE.write( 'Transition clock:'+htr.__str__()+'\n')
241
        for cla in cl_ds.clauses:
VIGNET Pierre's avatar
VIGNET Pierre committed
242
243
244
245
            TRACE_FILE.write( cla.__str__()+'\n')
        mess =  'free clocks registered:'+ cl_ds.free_clocks.__str__()+'\n'
        TRACE_FILE.write(mess)
        TRACE_FILE.write( 'reporter: '+ reporter.mess+'\n')
246

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

VIGNET Pierre's avatar
VIGNET Pierre committed
261
262
263
264
265
266
267
268
        tvisit = TableVisitor(None) # no error display
        model.accept(tvisit)
        reporter = ErrorRep()
        cl_ds = CLDynSys( tvisit.tab_symb, None)
        TRACE_FILE.write('\ntestPermCondEvent')
        TRACE_FILE.write( '\n\nn1/p --> n2; h[n4]' +'\n')
        htr = gen_transition_clock(trans, cl_ds, None, reporter)
        TRACE_FILE.write( 'Transition clock:'+ htr.__str__()+'\n')
269
        for cla in cl_ds.clauses:
VIGNET Pierre's avatar
VIGNET Pierre committed
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
            TRACE_FILE.write(cla.__str__()+'\n')
        mess = 'free clocks registered:'+ cl_ds.free_clocks.__str__()+'\n'
        TRACE_FILE.write(mess)
        TRACE_FILE.write( 'reporter: '+ reporter.mess+'\n')

    def test_input_cond_event(self): #OK
        """
        n4/i;
        n1/i --> n2; h[n4];
        """
        model = ChartModel("Test")
        root = model.get_root()
        nn1 = root.add_input_node('n1', 0, 0)
        nn2 = root.add_simple_node('n2', 0, 0)
        nn4 = root.add_input_node('n4', 0, 0)
        trans = root.add_transition(nn1, nn2)
        trans.set_condition("n4")
        trans.set_event('h')
288

VIGNET Pierre's avatar
VIGNET Pierre committed
289
290
291
292
293
294
        tvisit = TableVisitor(None) # no error display
        model.accept(tvisit)
        reporter = ErrorRep()
        cl_ds = CLDynSys( tvisit.tab_symb, None)
        TRACE_FILE.write('\ntestInputCondEvent')
        TRACE_FILE.write( '\n\nn1/i --> n2; h[n4]'+'\n')
295
        htr = gen_transition_clock(trans, cl_ds, None, reporter)
VIGNET Pierre's avatar
VIGNET Pierre committed
296
        TRACE_FILE.write( 'Transition clock:' +htr.__str__()+'\n')
297
        for cla in cl_ds.clauses:
VIGNET Pierre's avatar
VIGNET Pierre committed
298
299
300
301
            TRACE_FILE.write( cla.__str__()+'\n')
        mess = 'free clocks registered:'+ cl_ds.free_clocks.__str__()+'\n'
        TRACE_FILE.write(mess)
        TRACE_FILE.write( 'reporter: '+ reporter.mess+'\n')
302

VIGNET Pierre's avatar
VIGNET Pierre committed
303
304
305
306
307
308
309
310
311
312
313
314
315
    # complex events
    def test_no_cond_event_when1(self): #OK
        """
        n1 --> n2; h when n3[]
        n3;
        """
        model = ChartModel("Test")
        root = model.get_root()
        nn1 = root.add_simple_node('n1', 0, 0)
        nn2 = root.add_simple_node('n2', 0, 0)
        nn3 = root.add_simple_node('n3', 0, 0)
        trans = root.add_transition(nn1, nn2)
        trans.set_event('h when n3')
316

VIGNET Pierre's avatar
VIGNET Pierre committed
317
318
319
320
321
        tvisit = TableVisitor(None) # no error display
        model.accept(tvisit)
        reporter = ErrorRep()
        cl_ds = CLDynSys(tvisit.tab_symb, reporter)
        TRACE_FILE.write('\ntestNoCondEventWhen1')
322
        TRACE_FILE.write( '\n\nn1 --> n2; h when n3[]; n3;'+'\n')
VIGNET Pierre's avatar
VIGNET Pierre committed
323
324
        htr = gen_transition_clock(trans, cl_ds, None, reporter)
        TRACE_FILE.write( 'Transition clock:'+ htr.__str__()+'\n')
325
        for cla in cl_ds.clauses:
VIGNET Pierre's avatar
VIGNET Pierre committed
326
327
328
329
330
            TRACE_FILE.write( cla.__str__()+'\n')
        mess = 'free clocks registered:' +cl_ds.free_clocks.__str__()+'\n'
        TRACE_FILE.write(mess)
        TRACE_FILE.write( 'place_clocks'+ cl_ds.place_clocks.__str__()+'\n')
        TRACE_FILE.write( 'reporter: '+ reporter.mess+'\n')
331

VIGNET Pierre's avatar
VIGNET Pierre committed
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
    def test_no_cond_event_when2(self): #OK
        """
        n1 --> n2; h when n3[]
        n3 --> n1 ; h2 when h[]
        Error h is not a state
        """
        model = ChartModel("Test")
        root = model.get_root()
        nn1 = root.add_simple_node('n1', 0, 0)
        nn2 = root.add_simple_node('n2', 0, 0)
        nn3 = root.add_simple_node('n3', 0, 0)
        tr1 = root.add_transition(nn1, nn2)
        tr1.set_event('h when n3')
        tr2 = root.add_transition(nn3, nn1)
        tr2.set_event('h2 when h')
347

VIGNET Pierre's avatar
VIGNET Pierre committed
348
349
350
        reporter = ErrorRep()
        tvisit = TableVisitor(reporter) # no error display
        model.accept(tvisit)
351

VIGNET Pierre's avatar
VIGNET Pierre committed
352
353
354
        cl_ds = CLDynSys(tvisit.tab_symb, reporter)
        TRACE_FILE.write('\ntestNoCondEventWhen1')
        mess =  '\n\nn1 --> n2; h when n3[]; n3 --> n1 ; h2 when h[];'+'\n'
355
        TRACE_FILE.write(mess)
VIGNET Pierre's avatar
VIGNET Pierre committed
356
357
358
359
        htr = gen_transition_clock(tr1, cl_ds, None, reporter)
        TRACE_FILE.write( 'Transition clock:'+ htr.__str__()+'\n')
        htr = gen_transition_clock(tr2, cl_ds, None, reporter)
        TRACE_FILE.write( 'Transition clock:'+ htr.__str__()+'\n')
360
        for cla in cl_ds.clauses:
VIGNET Pierre's avatar
VIGNET Pierre committed
361
362
363
364
365
            TRACE_FILE.write( cla.__str__()+'\n')
        mess =  'free clocks registered:' +cl_ds.free_clocks.__str__()+'\n'
        TRACE_FILE.write(mess)
        TRACE_FILE.write( 'place_clocks'+ cl_ds.place_clocks.__str__()+'\n')
        TRACE_FILE.write( 'reporter: '+ reporter.mess+'\n')
366

VIGNET Pierre's avatar
VIGNET Pierre committed
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
    def test_no_cond_event_when3(self): #OK
        """
        n1 --> n2; h when n3[]
        n3 --> n1 ; n2 when n1[]
        Error n2 is not a clock
        """
        model = ChartModel("Test")
        root = model.get_root()
        nn1 = root.add_simple_node('n1', 0, 0)
        nn2 = root.add_simple_node('n2', 0, 0)
        nn3 = root.add_simple_node('n3', 0, 0)
        tr1 = root.add_transition(nn1, nn2)
        tr1.set_event('h when n3')
        tr2 = root.add_transition(nn3, nn1)
        tr2.set_event('n2 when n1')
382

VIGNET Pierre's avatar
VIGNET Pierre committed
383
384
385
        reporter = ErrorRep()
        tvisit = TableVisitor(reporter) # no error display
        model.accept(tvisit)
386

VIGNET Pierre's avatar
VIGNET Pierre committed
387
388
        cl_ds = CLDynSys(tvisit.tab_symb, reporter)
        TRACE_FILE.write('\ntestNoCondEventWhen1')
389
        TRACE_FILE.write( '\n\nn1 --> n2; n2 when n1[]; n3;'+'\n')
VIGNET Pierre's avatar
VIGNET Pierre committed
390
391
392
393
        htr = gen_transition_clock(tr1, cl_ds, None, reporter)
        TRACE_FILE.write( 'Transition clock:'+ htr.__str__()+'\n')
        htr = gen_transition_clock(tr2, cl_ds, None, reporter)
        TRACE_FILE.write( 'Transition clock:'+ htr.__str__()+'\n')
394
        for cla in cl_ds.clauses:
VIGNET Pierre's avatar
VIGNET Pierre committed
395
396
397
398
            TRACE_FILE.write( cla.__str__()+'\n')
        mess = 'free clocks registered:' +cl_ds.free_clocks.__str__()+'\n'
        TRACE_FILE.write(mess)
        TRACE_FILE.write( 'place_clocks'+ cl_ds.place_clocks.__str__()+'\n')
399
400
401
        TRACE_FILE.write( 'reporter: '+ reporter.mess+'\n')


VIGNET Pierre's avatar
VIGNET Pierre committed
402
403
404
405
406
407
408
409
410
411
412
413
414
    def test_no_cond_event_default(self): #OK
        """
        n1 --> n2; h1 when c1 default h2[c3]
        """
        model = ChartModel("Test")
        root = model.get_root()
        nn1 = root.add_simple_node('n1', 0, 0)
        nn2 = root.add_simple_node('n2', 0, 0)
        root.add_simple_node('c1', 0, 0)
        root.add_simple_node('c3', 0, 0)
        tr1 = root.add_transition(nn1, nn2)
        tr1.set_event('h when c1 default h2')
        tr1.set_condition('c3')
415

VIGNET Pierre's avatar
VIGNET Pierre committed
416
417
418
        reporter = ErrorRep()
        tvisit = TableVisitor(reporter) # no error display
        model.accept(tvisit)
419

VIGNET Pierre's avatar
VIGNET Pierre committed
420
421
        cl_ds = CLDynSys(tvisit.tab_symb, reporter)
        TRACE_FILE.write('\ntestNoCondEventWhen1')
422
        TRACE_FILE.write( '\n\nn1 --> n2; n2 when n1[]; n3;'+'\n')
VIGNET Pierre's avatar
VIGNET Pierre committed
423
424
425
        htr = gen_transition_clock(tr1, cl_ds, None, reporter)
        TRACE_FILE.write( 'Transition clock:'+ htr.__str__()+'\n')

426
        for cla in cl_ds.clauses:
VIGNET Pierre's avatar
VIGNET Pierre committed
427
428
429
430
            TRACE_FILE.write( cla.__str__()+'\n')
        mess =  'free clocks registered:' +cl_ds.free_clocks.__str__()+'\n'
        TRACE_FILE.write(mess)
        TRACE_FILE.write( 'place_clocks'+ cl_ds.place_clocks.__str__()+'\n')
431
432
433
        TRACE_FILE.write( 'reporter: '+ reporter.mess+'\n')


VIGNET Pierre's avatar
VIGNET Pierre committed
434
435
436
class TestTransitionList(unittest.TestCase):
    """
    As it says
437
438
    """

VIGNET Pierre's avatar
VIGNET Pierre committed
439
440
441
#    def setUp(self):
#        self.output = open('TestTransition.txt')
#        #self.output = sys.stdout
442
443


VIGNET Pierre's avatar
VIGNET Pierre committed
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
    def test_no_cond_on_out2events(self):
        """
        n1 --> n2; h1[not n4]
        n1 --> n3; h2[]
        n4 --> n1; h3[]
        gen_transition_list_clock tested
        """
        model = ChartModel("Test")
        root = model.get_root()
        nn1 = root.add_simple_node('n1', 0, 0)
        nn2 = root.add_simple_node('n2', 0, 0)
        nn3 = root.add_simple_node('n3', 0, 0)
        nn4 = root.add_simple_node('n4', 0, 0)
        trans = root.add_transition(nn1, nn2)
        trans.set_condition("not n4")
        trans.set_event('h1')
        trans = root.add_transition(nn1, nn3)
        trans.set_event('h2')
        trans = root.add_transition(nn4, nn1)
        trans.set_event('h3')
464

VIGNET Pierre's avatar
VIGNET Pierre committed
465
466
467
468
469
470
471
472
473
474
        tvisit = TableVisitor(None) # no error display/ might crash
        model.accept(tvisit)
        TRACE_FILE.write('\ntestNoCondOnOut2Events')
        mess = '\n\nn1 --> n2; h1[not n4] \nn1 --> n3; h2[]\nn4 --> n1; h3[]\n'
        TRACE_FILE.write(mess)
        reporter = ErrorRep()
        cl_ds = CLDynSys( tvisit.tab_symb, None)
        trl = nn1.outgoing_trans
        sed = dict()
        htr = gen_transition_list_clock(trl, cl_ds, sed, reporter)
475
        TRACE_FILE.write( 'Transition clock:' +htr.__str__()+'\n')
476
477
        TRACE_FILE.write( 'NB Clauses:' +str(len(cl_ds.clauses))+'\n')
        for cla in cl_ds.clauses:
VIGNET Pierre's avatar
VIGNET Pierre committed
478
479
480
            TRACE_FILE.write( cla.__str__()+'\n')
        mess = 'free clocks registered:'+cl_ds.free_clocks.__str__()+'\n'
        TRACE_FILE.write(mess)
481

VIGNET Pierre's avatar
VIGNET Pierre committed
482
483
484
485
486
487
488
489
490
491
    def test_very_simple(self): #OK to optimize
        """
        n1 --> n2; []
        """
        model = ChartModel("Test")
        root = model.get_root()
        nn1 = root.add_simple_node('n1', 0, 0)
        nn2 = root.add_simple_node('n2', 0, 0)
        trans = root.add_transition(nn1, nn2)

492

VIGNET Pierre's avatar
VIGNET Pierre committed
493
494
495
496
497
498
499
        model.clean_code()
        tvisit = TableVisitor(None) # no error display
        model.accept(tvisit)
        reporter = ErrorRep()
        cl_ds = CLDynSys( tvisit.tab_symb, None)
        TRACE_FILE.write('\ntestVerySimple')
        TRACE_FILE.write( '\n\nn1 --> n2; [] \n')
500
        gen_simple_evolution(nn1, cl_ds, None, reporter)
501
        for cla in cl_ds.clauses:
VIGNET Pierre's avatar
VIGNET Pierre committed
502
503
504
505
            TRACE_FILE.write( cla.__str__()+'\n')
        mess =  'free clocks registered:'+cl_ds.free_clocks.__str__()+'\n'
        TRACE_FILE.write(mess)
        model.clean_code()
506

VIGNET Pierre's avatar
VIGNET Pierre committed
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
    def test_simple(self):
        """
        n1 --> n2; h1[not n4]
        n1 --> n3; h2[]
        n4 --> n1; h3[]
        """
        model = ChartModel("Test")
        root = model.get_root()
        nn1 = root.add_simple_node('n1', 0, 0)
        nn2 = root.add_simple_node('n2', 0, 0)
        nn3 = root.add_simple_node('n3', 0, 0)
        nn4 = root.add_simple_node('n4', 0, 0)
        trans = root.add_transition(nn1, nn2)
        trans.set_condition("not n4")
        trans.set_event('h1')
        trans = root.add_transition(nn1, nn3)
        trans.set_event('h2')
        trans = root.add_transition(nn4, nn1)
        trans.set_event('h3')
526

VIGNET Pierre's avatar
VIGNET Pierre committed
527
528
529
530
531
532
533
534
535
        model.clean_code()
        tvisit = TableVisitor(None) # no error display
        model.accept(tvisit)
        reporter = ErrorRep()
        cl_ds = CLDynSys( tvisit.tab_symb, None)
        TRACE_FILE.write('\ntestSimple')
        mess =  '\n\nn1 --> n2; h1[not n4] \nn1 --> n3; h2[]\nn4 --> n1; h3[]\n'
        TRACE_FILE.write(mess)
        sed = dict()
536
        gen_simple_evolution(nn1, cl_ds, sed, reporter)
537
538
        TRACE_FILE.write( 'NB Clauses:' + str(len(cl_ds.clauses)) + '\n')
        for cla in cl_ds.clauses:
VIGNET Pierre's avatar
VIGNET Pierre committed
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
            TRACE_FILE.write( cla.__str__() + '\n')
        mess = 'free clocks registered:'+ cl_ds.free_clocks.__str__()+'\n'
        TRACE_FILE.write(mess)
        model.clean_code()

    def test_simple_in_no_out(self):
        """
        n2 --> n1; h1[not n4]
        n4 --> n1; h3[]
        """
        model = ChartModel("Test")
        root = model.get_root()
        nn1 = root.add_simple_node('n1', 0, 0)
        nn2 = root.add_simple_node('n2', 0, 0)
        nn3 = root.add_simple_node('n3', 0, 0)
        nn4 = root.add_simple_node('n4', 0, 0)
        trans = root.add_transition(nn2, nn1)
        trans.set_condition("not n4")
        trans.set_event('h1')
        trans = root.add_transition(nn4, nn1)
        trans.set_event('h3')
560

VIGNET Pierre's avatar
VIGNET Pierre committed
561
562
563
564
565
566
        tvisit = TableVisitor(None) # no error display
        model.accept(tvisit)
        reporter = ErrorRep()
        cl_ds = CLDynSys( tvisit.tab_symb, reporter)
        TRACE_FILE.write('\ntestSimpleInNoOut')
        TRACE_FILE.write( '\n\nn2 --> n1; h1[not n4] \nn4 --> n1; h3[]\n')
567
        gen_simple_evolution(nn1, cl_ds, None, reporter)
568
        for cla in cl_ds.clauses:
VIGNET Pierre's avatar
VIGNET Pierre committed
569
570
571
            TRACE_FILE.write( cla.__str__()+'\n')
        mess =  'free clocks registered:' + cl_ds.free_clocks.__str__() + '\n'
        TRACE_FILE.write(mess)
572

VIGNET Pierre's avatar
VIGNET Pierre committed
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
    def test_simple_out_no_in(self):
        """
        n1 --> n2; h1[not n4]
        n1 --> n3; h2[]
        """
        model = ChartModel("Test")
        root = model.get_root()
        nn1 = root.add_simple_node('n1', 0, 0)
        nn2 = root.add_simple_node('n2', 0, 0)
        nn3 = root.add_simple_node('n3', 0, 0)
        nn4 = root.add_simple_node('n4', 0, 0)
        trans = root.add_transition(nn1, nn2)
        trans.set_condition("not n4")
        trans.set_event('h1')
        trans = root.add_transition(nn1, nn3)
        trans.set_event('h2')
589

VIGNET Pierre's avatar
VIGNET Pierre committed
590
591
592
593
594
595
596
        model.clean_code()
        tvisit = TableVisitor(None) # no error display
        model.accept(tvisit)
        reporter = ErrorRep()
        cl_ds = CLDynSys( tvisit.tab_symb, None)
        TRACE_FILE.write('\ntestSimpleOutNoIn')
        TRACE_FILE.write( '\n\nn1 --> n2; h1[not n4] \nn1 --> n3; '+'\n')
597
        gen_simple_evolution(nn1, cl_ds, None, reporter)
598
        for cla in cl_ds.clauses:
VIGNET Pierre's avatar
VIGNET Pierre committed
599
600
601
            TRACE_FILE.write( cla.__str__()+'\n')
        mess =  'free clocks registered:'+ cl_ds.free_clocks.__str__()+'\n'
        TRACE_FILE.write(mess)
602

VIGNET Pierre's avatar
VIGNET Pierre committed
603
604
605
606
607
608
609
610
611
612
613
614
615
616
    def test_simple_no_trans(self): #OK
        """
        n1;
        """
        model = ChartModel("Test")
        root = model.get_root()
        nn1 = root.add_simple_node('n1', 0, 0)

        tvisit = TableVisitor(None) # no error display
        model.accept(tvisit)
        reporter = ErrorRep()
        cl_ds = CLDynSys( tvisit.tab_symb, None)
        TRACE_FILE.write('\ntestSimpleNoTrans')
        TRACE_FILE.write( '\n\nn1; \n')
617
        gen_simple_evolution(nn1, cl_ds, None, reporter)
618
        for cla in cl_ds.clauses:
VIGNET Pierre's avatar
VIGNET Pierre committed
619
620
621
            TRACE_FILE.write( cla.__str__() + '\n')
        mess = 'free clocks registered:' + cl_ds.free_clocks.__str__() + '\n'
        TRACE_FILE.write(mess)
622
623


VIGNET Pierre's avatar
VIGNET Pierre committed
624
625
626
627
class TestFull(unittest.TestCase):
    """
    test full models
    """
628

VIGNET Pierre's avatar
VIGNET Pierre committed
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
    def test_model1(self):
        """
        n1 --> n2; h1[not n4]
        n1 --> n3; h2[]
        n4 --> n1; h3[]
        """
        model = ChartModel("Test")
        root = model.get_root()
        nn1 = root.add_simple_node('n1', 0, 0)
        nn2 = root.add_simple_node('n2', 0, 0)
        nn3 = root.add_simple_node('n3', 0, 0)
        nn4 = root.add_simple_node('n4', 0, 0)
        trans = root.add_transition(nn1, nn2)
        trans.set_condition("not n4")
        trans.set_event('h1')
        trans = root.add_transition(nn1, nn3)
        trans.set_event('h2')
        trans = root.add_transition(nn4, nn1)
        trans.set_event('h3')
648

VIGNET Pierre's avatar
VIGNET Pierre committed
649
650
651
652
653
654
655
656
        tvisit = TableVisitor(None) # no error display
        model.accept(tvisit)
        reporter = ErrorRep()
        cl_ds = CLDynSys( tvisit.tab_symb, reporter)
        TRACE_FILE.write('\ntestModel1')
        mess = '\n\nn1 --> n2; h1[not n4] \nn1 --> n3; h2[]\nn4 --> n1; h3[]\n'
        TRACE_FILE.write(mess)
        gt2clauses = GT2Clauses(cl_ds, False, reporter)
657
        model.accept(gt2clauses)
658
659
        TRACE_FILE.write( 'NB Clauses:' +str(len(cl_ds.clauses))+'\n')
        for cla in cl_ds.clauses:
VIGNET Pierre's avatar
VIGNET Pierre committed
660
661
662
663
664
665
            TRACE_FILE.write( cla.__str__()+'\n')
        TRACE_FILE.write( 'variables'+ cl_ds.base_var_set.__str__()+'\n')
        mess = 'free clocks registered:'+ cl_ds.free_clocks.__str__()+'\n'
        TRACE_FILE.write(mess)
        TRACE_FILE.write( 'place_clocks'+ cl_ds.place_clocks.__str__()+'\n')
        TRACE_FILE.write( 'inputs'+ cl_ds.inputs.__str__()+'\n')
666

VIGNET Pierre's avatar
VIGNET Pierre committed
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
    def test_model2(self): #OK
        """
        n1 --> n2; h1 when n2 default h2[not n4]
        n1 --> n3; h2 when n4[]
        n4 --> n1; h3[]
        """
        model = ChartModel("Test")
        root = model.get_root()
        nn1 = root.add_simple_node('n1', 0, 0)
        nn2 = root.add_simple_node('n2', 0, 0)
        nn3 = root.add_simple_node('n3', 0, 0)
        nn4 = root.add_simple_node('n4', 0, 0)
        trans = root.add_transition(nn1, nn2)
        trans.set_condition("not n4")
        trans.set_event('h1 when n2 default h2')
        trans = root.add_transition(nn1, nn3)
        trans.set_event('h2 when n4')
        trans = root.add_transition(nn4, nn1)
        trans.set_event('h3')
686

VIGNET Pierre's avatar
VIGNET Pierre committed
687
688
689
690
691
692
693
694
695
        tvisit = TableVisitor(None) # no error display
        model.accept(tvisit)
        reporter = ErrorRep()
        cl_ds = CLDynSys( tvisit.tab_symb, reporter)
        TRACE_FILE.write('\ntestModel2')
        mess =  '\n\nn1 --> n2; h1 when n2 default h2[not n4]'
        mess = mess + '\nn1 --> n3; h2 when n4[]\nn4 --> n1; h3[]\n'
        TRACE_FILE.write(mess)
        gt2clauses = GT2Clauses(cl_ds, reporter, False)
696
        model.accept(gt2clauses)
697
        for cla in cl_ds.clauses:
VIGNET Pierre's avatar
VIGNET Pierre committed
698
699
700
701
702
703
            TRACE_FILE.write( cla.__str__()+'\n')
        TRACE_FILE.write( 'variables'+ cl_ds.base_var_set.__str__()+'\n')
        mess = 'free clocks registered:'+ cl_ds.free_clocks.__str__()+'\n'
        TRACE_FILE.write(mess)
        TRACE_FILE.write( 'place_clocks'+ cl_ds.place_clocks.__str__()+'\n')
        TRACE_FILE.write( 'inputs'+ cl_ds.inputs.__str__()+'\n')
704
705


VIGNET Pierre's avatar
VIGNET Pierre committed
706
707
708
709
710
711
712
713
714
715
716
717
718
    def test_model3(self): #OK
        """
        n4;
        n1/p --> n2; h[n4];
        """
        model = ChartModel("Test")
        root = model.get_root()
        nn1 = root.add_perm_node('n1', 0, 0)
        nn2 = root.add_simple_node('n2', 0, 0)
        nn4 = root.add_simple_node('n4', 0, 0)
        trans = root.add_transition(nn1, nn2)
        trans.set_condition("n4")
        trans.set_event('h')
719

VIGNET Pierre's avatar
VIGNET Pierre committed
720
721
722
723
724
725
        tvisit = TableVisitor(None) # no error display
        model.accept(tvisit)
        reporter = ErrorRep()
        cl_ds = CLDynSys( tvisit.tab_symb, None)
        TRACE_FILE.write('\ntestInputCondEvent')
        TRACE_FILE.write( '\n\nn4; \nn1/p --> n2; h[n4]'+'\n')
726

VIGNET Pierre's avatar
VIGNET Pierre committed
727
728
729
730
731
732
733
        tvisit = TableVisitor(None) # no error display
        model.accept(tvisit)
        reporter = ErrorRep()
        cl_ds = CLDynSys( tvisit.tab_symb, reporter)
        TRACE_FILE.write('\ntestModel2')
        TRACE_FILE.write( '\n\n\n')
        gt2clauses = GT2Clauses(cl_ds, reporter, False)
734
        model.accept(gt2clauses)
735
        for cla in cl_ds.clauses:
VIGNET Pierre's avatar
VIGNET Pierre committed
736
737
738
739
740
741
            TRACE_FILE.write( cla.__str__()+'\n')
        TRACE_FILE.write( 'variables'+ cl_ds.base_var_set.__str__()+'\n')
        mess =  'free clocks registered:'+ cl_ds.free_clocks.__str__()+'\n'
        TRACE_FILE.write(mess)
        TRACE_FILE.write( 'place_clocks'+ cl_ds.place_clocks.__str__()+'\n')
        TRACE_FILE.write( 'inputs'+ cl_ds.inputs.__str__()+'\n')
742
743


VIGNET Pierre's avatar
VIGNET Pierre committed
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
    def test_constraints(self):
        """
        As it says
        """
        model = ChartModel("Test")
        root = model.get_root()
        aaa = root.add_simple_node('A', 0, 0)
        bbb = root.add_simple_node('B', 0, 0)
        ccc = root.add_simple_node('C', 0, 0)
        ddd = root.add_simple_node('D', 0, 0)
        trans = root.add_transition(aaa, bbb)
        trans.set_event('h1 default h2')
        trans = root.add_transition(ccc, ddd)
        trans.set_event('h3')
        cont = 'synchro(h1, h3);\nexclus(h1, h2);\nincluded(h3, h2);'
        model.constraints = cont
        tvisit = TableVisitor(None) # no error display
        model.accept(tvisit)
        reporter = ErrorRep()
        cl_ds = CLDynSys( tvisit.tab_symb, reporter)
        gt2clauses = GT2Clauses(cl_ds, reporter, False)
765
        model.accept(gt2clauses)
766
        for cla in cl_ds.clauses:
VIGNET Pierre's avatar
VIGNET Pierre committed
767
768
769
770
771
            TRACE_FILE.write( cla.__str__()+'\n')
        TRACE_FILE.write( 'variables'+ cl_ds.base_var_set.__str__()+'\n')
        mess = 'free clocks registered:'+ cl_ds.free_clocks.__str__()+'\n'
        TRACE_FILE.write(mess)
        TRACE_FILE.write( 'place_clocks'+ cl_ds.place_clocks.__str__()+'\n')
772
773
        TRACE_FILE.write( 'inputs'+ cl_ds.inputs.__str__()+'\n')

774
775
776
777
778
779
    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"
780
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
781
        rep = ErrorRep()
782

VIGNET Pierre's avatar
VIGNET Pierre committed
783
        mcla = MCLAnalyser(rep)
784
785
786
787
788
789
        mcla.translator_opti = False
        filename = pkg_resources.resource_filename(
            __name__, # package name
            "../../guard_transitions/translators/tests/tgf_cano_noclock_cmp.cal"
        )
        mcla.build_from_cadlang(filename)
790
        nb_clauses_without_opti = len(mcla.dynamic_system.clauses)
791
        print("NB Clauses without opti:", nb_clauses_without_opti)
792

VIGNET Pierre's avatar
VIGNET Pierre committed
793
        mcla = MCLAnalyser(rep)
794
795
796
797
798
        filename = pkg_resources.resource_filename(
            __name__, # package name
            "../../guard_transitions/translators/tests/tgf_cano_noclock_cmp.cal"
        )
        mcla.build_from_cadlang(filename)
799
        nb_clauses_with_opti = len(mcla.dynamic_system.clauses)
800
        print("NB Clauses with opti:", nb_clauses_with_opti)
801
802
803
804

        assert nb_clauses_with_opti < nb_clauses_without_opti
        assert nb_clauses_with_opti == 1573
        assert nb_clauses_without_opti == 1909
805

VIGNET Pierre's avatar
VIGNET Pierre committed
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
class TestMCLSigExprVisitor (unittest.TestCase):
    """
    Test of signal expression
    """
    def test_ident1(self):
        """
        sigexp = xx
        """
        sexpr = SigIdentExpr('xx')
        cl_ds = CLDynSys(None, None)
        sexpv = MCLSigExprVisitor(cl_ds, 'Y', None)
        var = sexpr.accept(sexpv)
        TRACE_FILE.write( '\n\n sigexpr: xx'+'\n')
        TRACE_FILE.write( 'RETURN var (xx)'+ var.__str__()+'\n')
        TRACE_FILE.write( 'Clauses'+'\n')
821
        for cla in cl_ds.clauses:
VIGNET Pierre's avatar
VIGNET Pierre committed
822
            TRACE_FILE.write( cla.__str__()+'\n')
823

VIGNET Pierre's avatar
VIGNET Pierre committed
824
825
826
827
828
829
830
831
832
833
834
835
836
    def test_bin1(self):
        """
        X or Y
        """
        sexpr1 = SigIdentExpr('x')
        sexpr2 = SigIdentExpr('y')
        sexpr = SigSyncBinExpr('or', sexpr1, sexpr2)
        cl_ds = CLDynSys(None, None)
        sexpv = MCLSigExprVisitor(cl_ds, 'Z', dict())
        var = sexpr.accept(sexpv)
        TRACE_FILE.write( '\n\n sigexpr: X or Y'+'\n')
        TRACE_FILE.write( 'RETURN var (Z)'+ var.__str__()+'\n')
        TRACE_FILE.write( 'Clauses'+'\n')
837
        for cla in cl_ds.clauses:
VIGNET Pierre's avatar
VIGNET Pierre committed
838
            TRACE_FILE.write( cla.__str__()+'\n')
839

VIGNET Pierre's avatar
VIGNET Pierre committed
840
841
842
843
844
845
846
847
848
849
850
851
852
853
    def test_bin2(self):
        """
        X and Y
        """
        sexpr1 = SigIdentExpr('x')
        sexpr2 = SigIdentExpr('y')
        sexpr = SigSyncBinExpr('and', sexpr1, sexpr2)
        cl_ds = CLDynSys(None, None)
        sexpv = MCLSigExprVisitor(cl_ds, 'Z', dict())
        sexpv.output_lit = None # for output var generation
        var = sexpr.accept(sexpv)
        TRACE_FILE.writelines( '\n\n sigexpr: X and Y'+'\n')
        TRACE_FILE.write( 'RETURN var (aux var)'+ var.__str__()+'\n')
        TRACE_FILE.write( 'Clauses'+'\n')
854
        for cla in cl_ds.clauses:
VIGNET Pierre's avatar
VIGNET Pierre committed
855
            TRACE_FILE.write( cla.__str__()+'\n')
856

VIGNET Pierre's avatar
VIGNET Pierre committed
857
858
    def test_bin3(self):
        """
859
        h1 default h2
VIGNET Pierre's avatar
VIGNET Pierre committed
860
861
862
863
864
865
866
867
868
869
870
871
872
873
        """
        sexpr1 = SigIdentExpr('h1')
        sexpr2 = SigIdentExpr('h2')
        sexpr = SigDefaultExpr(sexpr1, sexpr2)
        symb_tab = dict()
        symb_tab['h1'] = ('clock', -1)
        symb_tab['h2'] = ('clock', -1)
        cl_ds = CLDynSys(symb_tab, None)
        sexpv = MCLSigExprVisitor(cl_ds, None)
        #sexpv.output_lit = None # for output var generation
        var = sexpr.accept(sexpv)
        TRACE_FILE.writelines( '\n\n sigexpr: h1 default h2'+'\n')
        TRACE_FILE.write( 'RETURN var (aux var)'+ var.__str__()+'\n')
        TRACE_FILE.write( 'Clauses'+'\n')
874
        for cla in cl_ds.clauses:
875
876
            TRACE_FILE.write( cla.__str__()+'\n')

VIGNET Pierre's avatar
VIGNET Pierre committed
877
878
    def test_bin4(self):
        """
879
        h1 when (a or b)
VIGNET Pierre's avatar
VIGNET Pierre committed
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
        """
        sexpr1 = SigIdentExpr('h1')
        sexpr2 = SigIdentExpr('h2')
        sexpr3 = SigIdentExpr('a')
        sexpr4 = SigIdentExpr('b')
        sexpr = SigSyncBinExpr('or', sexpr3, sexpr4)
        sexpr = SigWhenExpr(sexpr1, sexpr)
        symb_tab = dict()
        symb_tab['h1'] = ('clock', -1)
        symb_tab['h2'] = ('clock', -1)
        cl_ds = CLDynSys(symb_tab, None)
        sexpv = MCLSigExprVisitor(cl_ds, None)
        #sexpv.output_lit = None # for output var generation
        var = sexpr.accept(sexpv)
        TRACE_FILE.writelines( '\n\n sigexpr: h1 when (a or b)'+'\n')
        TRACE_FILE.write( 'RETURN var (aux var)'+ var.__str__()+'\n')
        TRACE_FILE.write( 'Clauses'+'\n')
897
        for cla in cl_ds.clauses:
898
899
            TRACE_FILE.write( cla.__str__()+'\n')

VIGNET Pierre's avatar
VIGNET Pierre committed
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
    def test_cse1(self):
        """
        common subexpression elimination
        h1 when (a or b) default h2 when (b or a)
        """
        sexpr1 = SigIdentExpr('h1')
        sexpr2 = SigIdentExpr('h2')
        sexpr3 = SigIdentExpr('a')
        sexpr4 = SigIdentExpr('b')
        a_or_b1 = SigSyncBinExpr('and', sexpr3, sexpr4)
        a_or_b2 = SigSyncBinExpr('and', sexpr4, sexpr3)
        hh1 = SigWhenExpr(sexpr1, a_or_b1)
        hh2 = SigWhenExpr(sexpr2, a_or_b2)
        sexpr = SigDefaultExpr(hh1, hh2)
        TRACE_FILE.write('Formula: ' + sexpr.__str__())
        symb_tab = dict()
        symb_tab['h1'] = ('clock', -1)
        symb_tab['h2'] = ('clock', -1)
        cl_ds = CLDynSys(symb_tab, None)
        sub_exp = dict()
        sexpv = MCLSigExprVisitor(cl_ds, None, sub_exp)
        #sexpv.output_lit = None # for output var generation
        var = sexpr.accept(sexpv)
        TRACE_FILE.write( '\n\n- RETURN var (aux var)'+ var.__str__()+'\n')
924
        TRACE_FILE.write('\n- NB Clauses:' + str(len(cl_ds.clauses)))
VIGNET Pierre's avatar
VIGNET Pierre committed
925
        TRACE_FILE.write( '\n- Clauses'+'\n')
926
        for cla in cl_ds.clauses:
927
928
            TRACE_FILE.write( cla.__str__()+'\n')

VIGNET Pierre's avatar
VIGNET Pierre committed
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
    def test_cse2(self):
        """
        common subexpression elimination
        h1 when (a or b) default h2 when (b or a)
        """
        hh1 = SigIdentExpr('h1')
        hh2 = SigIdentExpr('h2')
        h12 = SigDefaultExpr(hh1, hh2)
        h21 = SigDefaultExpr(hh2, hh1)
        sexpr = SigDefaultExpr(h12, h21)
        TRACE_FILE.write('Formula: ' + sexpr.__str__())
        symb_tab = dict()
        symb_tab['h1'] = ('clock', -1)
        symb_tab['h2'] = ('clock', -1)
        cl_ds = CLDynSys(symb_tab, None)
        sub_exp = dict()
        sexpv = MCLSigExprVisitor(cl_ds, None, sub_exp)
        #sexpv.output_lit = None # for output var generation
        var = sexpr.accept(sexpv)
        TRACE_FILE.write( '\n\n- RETURN var (aux var)'+ var.__str__()+'\n')
949
        TRACE_FILE.write('\n- NB Clauses:' + str(len(cl_ds.clauses)))
VIGNET Pierre's avatar
VIGNET Pierre committed
950
        TRACE_FILE.write( '\n- Clauses'+'\n')
951
        for cla in cl_ds.clauses:
952
953
954
955
            TRACE_FILE.write( cla.__str__()+'\n')



VIGNET Pierre's avatar
VIGNET Pierre committed
956
957
958
if __name__ == "__main__":
    #import sys;sys.argv = ['', 'Test.testName']
    unittest.main()
959

VIGNET Pierre's avatar
VIGNET Pierre committed
960
961
962
963
964
965
#    suiteFew = unittest.TestSuite()
    #suiteFew.addTest(TestMCLSigExprVisitor("testCSE2"))
    #suiteFew.addTest(Testgt2Sig("testOneTransCondEvent"))
    #suiteFew.addTest(TestTransitionClauses('testCondEvent'))
    #suiteFew.addTest(TestFull('testModel3'))
    #suiteFew.addTest(TestTransitionList("testSimple"))
966
    #unittest.TextTestRunner(verbosity=2).run(suiteFew)