TestMCLTranslators.py 35.2 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
VIGNET Pierre's avatar
VIGNET Pierre committed
46
47
48
import unittest
import sys

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


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

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

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

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

VIGNET Pierre's avatar
VIGNET Pierre committed
86
87
88
89
90
91
92
93
94
    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)
95

VIGNET Pierre's avatar
VIGNET Pierre committed
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
        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')
        for cla in cl_ds.list_clauses:
            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")
121

VIGNET Pierre's avatar
VIGNET Pierre committed
122
123
124
125
126
127
128
129
130
131
132
133
134
        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')
        for cla in cl_ds.list_clauses:
            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')
135

VIGNET Pierre's avatar
VIGNET Pierre committed
136
137
138
139
140
141
142
143
144
145
    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')
146

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

VIGNET Pierre's avatar
VIGNET Pierre committed
161
162
163
164
165
166
167
168
169
170
171
172
        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')
        for cla in cl_ds.list_clauses:
            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')
173

VIGNET Pierre's avatar
VIGNET Pierre committed
174
175
176
177
178
179
180
181
182
183
184
185
    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')
186

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

VIGNET Pierre's avatar
VIGNET Pierre committed
201
202
203
204
205
206
207
        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')
208
        TRACE_FILE.write( '\n\nn1 --> n2; h[not n3]'+'\n')
VIGNET Pierre's avatar
VIGNET Pierre committed
209
210
211
212
213
214
        htr = gen_transition_clock(trans, cl_ds, sed, reporter)
        TRACE_FILE.write( 'Transition clock:'+ htr.__str__()+'\n')
        for cla in cl_ds.list_clauses:
            TRACE_FILE.write( cla.__str__()+'\n')
        mess = 'free clocks registered:'+ cl_ds.free_clocks.__str__()+'\n'
        TRACE_FILE.write(mess)
215
216
217
218
219
220
        TRACE_FILE.write( 'reporter: '+ reporter.mess+'\n')





VIGNET Pierre's avatar
VIGNET Pierre committed
221
222
223
224
225
226
227
228
229
230
    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')
231

VIGNET Pierre's avatar
VIGNET Pierre committed
232
233
234
235
236
237
238
239
240
241
242
243
244
        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')
        for cla in cl_ds.list_clauses:
            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')
245

VIGNET Pierre's avatar
VIGNET Pierre committed
246
247
248
249
250
251
252
253
254
255
256
257
258
    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')
259

VIGNET Pierre's avatar
VIGNET Pierre committed
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
        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')
        for cla in cl_ds.list_clauses:
            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')
287

VIGNET Pierre's avatar
VIGNET Pierre committed
288
289
290
291
292
293
        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')
294
        htr = gen_transition_clock(trans, cl_ds, None, reporter)
VIGNET Pierre's avatar
VIGNET Pierre committed
295
296
297
298
299
300
        TRACE_FILE.write( 'Transition clock:' +htr.__str__()+'\n')
        for cla in cl_ds.list_clauses:
            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')
301

VIGNET Pierre's avatar
VIGNET Pierre committed
302
303
304
305
306
307
308
309
310
311
312
313
314
    # 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')
315

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

VIGNET Pierre's avatar
VIGNET Pierre committed
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
    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')
346

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

VIGNET Pierre's avatar
VIGNET Pierre committed
351
352
353
        cl_ds = CLDynSys(tvisit.tab_symb, reporter)
        TRACE_FILE.write('\ntestNoCondEventWhen1')
        mess =  '\n\nn1 --> n2; h when n3[]; n3 --> n1 ; h2 when h[];'+'\n'
354
        TRACE_FILE.write(mess)
VIGNET Pierre's avatar
VIGNET Pierre committed
355
356
357
358
359
360
361
362
363
364
        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')
        for cla in cl_ds.list_clauses:
            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')
365

VIGNET Pierre's avatar
VIGNET Pierre committed
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
    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')
381

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

VIGNET Pierre's avatar
VIGNET Pierre committed
386
387
        cl_ds = CLDynSys(tvisit.tab_symb, reporter)
        TRACE_FILE.write('\ntestNoCondEventWhen1')
388
        TRACE_FILE.write( '\n\nn1 --> n2; n2 when n1[]; n3;'+'\n')
VIGNET Pierre's avatar
VIGNET Pierre committed
389
390
391
392
393
394
395
396
397
        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')
        for cla in cl_ds.list_clauses:
            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')
398
399
400
        TRACE_FILE.write( 'reporter: '+ reporter.mess+'\n')


VIGNET Pierre's avatar
VIGNET Pierre committed
401
402
403
404
405
406
407
408
409
410
411
412
413
    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')
414

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

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

        for cla in cl_ds.list_clauses:
            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')
430
431
432
        TRACE_FILE.write( 'reporter: '+ reporter.mess+'\n')


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

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


VIGNET Pierre's avatar
VIGNET Pierre committed
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
    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')
463

VIGNET Pierre's avatar
VIGNET Pierre committed
464
465
466
467
468
469
470
471
472
473
        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)
474
        TRACE_FILE.write( 'Transition clock:' +htr.__str__()+'\n')
VIGNET Pierre's avatar
VIGNET Pierre committed
475
476
477
478
479
        TRACE_FILE.write( 'NB Clauses:' +str(len(cl_ds.list_clauses))+'\n')
        for cla in cl_ds.list_clauses:
            TRACE_FILE.write( cla.__str__()+'\n')
        mess = 'free clocks registered:'+cl_ds.free_clocks.__str__()+'\n'
        TRACE_FILE.write(mess)
480

VIGNET Pierre's avatar
VIGNET Pierre committed
481
482
483
484
485
486
487
488
489
490
    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)

491

VIGNET Pierre's avatar
VIGNET Pierre committed
492
493
494
495
496
497
498
        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')
499
        gen_simple_evolution(nn1, cl_ds, None, reporter)
VIGNET Pierre's avatar
VIGNET Pierre committed
500
501
502
503
504
        for cla in cl_ds.list_clauses:
            TRACE_FILE.write( cla.__str__()+'\n')
        mess =  'free clocks registered:'+cl_ds.free_clocks.__str__()+'\n'
        TRACE_FILE.write(mess)
        model.clean_code()
505

VIGNET Pierre's avatar
VIGNET Pierre committed
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
    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')
525

VIGNET Pierre's avatar
VIGNET Pierre committed
526
527
528
529
530
531
532
533
534
        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()
535
        gen_simple_evolution(nn1, cl_ds, sed, reporter)
VIGNET Pierre's avatar
VIGNET Pierre committed
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
        TRACE_FILE.write( 'NB Clauses:' + str(len(cl_ds.list_clauses)) + '\n')
        for cla in cl_ds.list_clauses:
            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')
559

VIGNET Pierre's avatar
VIGNET Pierre committed
560
561
562
563
564
565
        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')
566
        gen_simple_evolution(nn1, cl_ds, None, reporter)
VIGNET Pierre's avatar
VIGNET Pierre committed
567
568
569
570
        for cla in cl_ds.list_clauses:
            TRACE_FILE.write( cla.__str__()+'\n')
        mess =  'free clocks registered:' + cl_ds.free_clocks.__str__() + '\n'
        TRACE_FILE.write(mess)
571

VIGNET Pierre's avatar
VIGNET Pierre committed
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
    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')
588

VIGNET Pierre's avatar
VIGNET Pierre committed
589
590
591
592
593
594
595
        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')
596
        gen_simple_evolution(nn1, cl_ds, None, reporter)
VIGNET Pierre's avatar
VIGNET Pierre committed
597
598
599
600
        for cla in cl_ds.list_clauses:
            TRACE_FILE.write( cla.__str__()+'\n')
        mess =  'free clocks registered:'+ cl_ds.free_clocks.__str__()+'\n'
        TRACE_FILE.write(mess)
601

VIGNET Pierre's avatar
VIGNET Pierre committed
602
603
604
605
606
607
608
609
610
611
612
613
614
615
    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')
616
        gen_simple_evolution(nn1, cl_ds, None, reporter)
VIGNET Pierre's avatar
VIGNET Pierre committed
617
618
619
620
        for cla in cl_ds.list_clauses:
            TRACE_FILE.write( cla.__str__() + '\n')
        mess = 'free clocks registered:' + cl_ds.free_clocks.__str__() + '\n'
        TRACE_FILE.write(mess)
621
622


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

VIGNET Pierre's avatar
VIGNET Pierre committed
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
    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')
647

VIGNET Pierre's avatar
VIGNET Pierre committed
648
649
650
651
652
653
654
655
        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)
656
        model.accept(gt2clauses)
VIGNET Pierre's avatar
VIGNET Pierre committed
657
658
659
660
661
662
663
664
        TRACE_FILE.write( 'NB Clauses:' +str(len(cl_ds.list_clauses))+'\n')
        for cla in cl_ds.list_clauses:
            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')
665

VIGNET Pierre's avatar
VIGNET Pierre committed
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
    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')
685

VIGNET Pierre's avatar
VIGNET Pierre committed
686
687
688
689
690
691
692
693
694
        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)
695
        model.accept(gt2clauses)
VIGNET Pierre's avatar
VIGNET Pierre committed
696
697
698
699
700
701
702
        for cla in cl_ds.list_clauses:
            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')
703
704


VIGNET Pierre's avatar
VIGNET Pierre committed
705
706
707
708
709
710
711
712
713
714
715
716
717
    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')
718

VIGNET Pierre's avatar
VIGNET Pierre committed
719
720
721
722
723
724
        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')
725

VIGNET Pierre's avatar
VIGNET Pierre committed
726
727
728
729
730
731
732
        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)
733
        model.accept(gt2clauses)
VIGNET Pierre's avatar
VIGNET Pierre committed
734
735
736
737
738
739
740
        for cla in cl_ds.list_clauses:
            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')
741
742


VIGNET Pierre's avatar
VIGNET Pierre committed
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
    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)
764
        model.accept(gt2clauses)
VIGNET Pierre's avatar
VIGNET Pierre committed
765
766
767
768
769
770
        for cla in cl_ds.list_clauses:
            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')
771
772
        TRACE_FILE.write( 'inputs'+ cl_ds.inputs.__str__()+'\n')

773
    @unittest.skip("Test files not provided")
VIGNET Pierre's avatar
VIGNET Pierre committed
774
775
776
    def test_tgf_no_clock(self):
        """
        optimisation gain comparison
777
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
778
779
780
781
        rep = ErrorRep()
        mcla = MCLAnalyser(rep)
        mcla.opti = False
        mcla.build_from_chart_file("../ucl/examples/test_tgfb_ref_300511.bcx")
782
        mess = '\n- NB Clauses:' + str(len(mcla.dynamical_system.list_clauses))
VIGNET Pierre's avatar
VIGNET Pierre committed
783
784
785
        TRACE_FILE.write(mess)
        mcla = MCLAnalyser(rep)
        mcla.build_from_chart_file("../ucl/examples/test_tgfb_ref_300511.bcx")
786
        mess = '\n- NB Clauses:' + str(len(mcla.dynamical_system.list_clauses))
VIGNET Pierre's avatar
VIGNET Pierre committed
787
        TRACE_FILE.write(mess)
788

VIGNET Pierre's avatar
VIGNET Pierre committed
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
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')
        for cla in cl_ds.list_clauses:
            TRACE_FILE.write( cla.__str__()+'\n')
806

VIGNET Pierre's avatar
VIGNET Pierre committed
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
    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')
        for cla in cl_ds.list_clauses:
            TRACE_FILE.write( cla.__str__()+'\n')
822

VIGNET Pierre's avatar
VIGNET Pierre committed
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
    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')
        for cla in cl_ds.list_clauses:
            TRACE_FILE.write( cla.__str__()+'\n')
839

VIGNET Pierre's avatar
VIGNET Pierre committed
840
841
    def test_bin3(self):
        """
842
        h1 default h2
VIGNET Pierre's avatar
VIGNET Pierre committed
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
        """
        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')
        for cla in cl_ds.list_clauses:
858
859
            TRACE_FILE.write( cla.__str__()+'\n')

VIGNET Pierre's avatar
VIGNET Pierre committed
860
861
    def test_bin4(self):
        """
862
        h1 when (a or b)
VIGNET Pierre's avatar
VIGNET Pierre committed
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
        """
        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')
        for cla in cl_ds.list_clauses:
881
882
            TRACE_FILE.write( cla.__str__()+'\n')

VIGNET Pierre's avatar
VIGNET Pierre committed
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
    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')
        TRACE_FILE.write('\n- NB Clauses:' + str(len(cl_ds.list_clauses)))
        TRACE_FILE.write( '\n- Clauses'+'\n')
        for cla in cl_ds.list_clauses:
910
911
            TRACE_FILE.write( cla.__str__()+'\n')

VIGNET Pierre's avatar
VIGNET Pierre committed
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
    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')
        TRACE_FILE.write('\n- NB Clauses:' + str(len(cl_ds.list_clauses)))
        TRACE_FILE.write( '\n- Clauses'+'\n')
        for cla in cl_ds.list_clauses:
935
936
937
938
            TRACE_FILE.write( cla.__str__()+'\n')



VIGNET Pierre's avatar
VIGNET Pierre committed
939
940
941
if __name__ == "__main__":
    #import sys;sys.argv = ['', 'Test.testName']
    unittest.main()
942

VIGNET Pierre's avatar
VIGNET Pierre committed
943
944
945
946
947
948
#    suiteFew = unittest.TestSuite()
    #suiteFew.addTest(TestMCLSigExprVisitor("testCSE2"))
    #suiteFew.addTest(Testgt2Sig("testOneTransCondEvent"))
    #suiteFew.addTest(TestTransitionClauses('testCondEvent'))
    #suiteFew.addTest(TestFull('testModel3'))
    #suiteFew.addTest(TestTransitionList("testSimple"))
949
    #unittest.TextTestRunner(verbosity=2).run(suiteFew)