mealy_testscenario.py 1.21 KB
Newer Older
Rick Smetsers's avatar
Rick Smetsers committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26


import collections

from z3gi.model.ra import Action



"""Test scenarios contain a list of traces together with the number of locations and registers of the SUT generating
 these traces.
"""
MealyTestCase = collections.namedtuple('MealyTestCase', 'description traces nr_states')

sut_m1 = MealyTestCase("output '1' if the length of the trace so far is even, else output '0'",
                        [(('a', '0'), ('a', '1'), ('a', '0'), ('a', '1')),
                         (('a', '0'), ('a', '1'), ('a', '0'), ('b', '1')),
                         (('a', '0'), ('a', '1'), ('b', '0'), ('a', '1')),
                         (('a', '0'), ('b', '1'), ('a', '0'), ('a', '1')),
                         (('b', '0'), ('a', '1'), ('a', '0'), ('a', '1')),
                         (('a', '0'), ('a', '1'), ('b', '0'), ('b', '1')),
                         (('a', '0'), ('b', '1'), ('b', '0'), ('a', '1')),
                         (('b', '0'), ('b', '1'), ('a', '0'), ('a', '1')),
                         (('a', '0'), ('b', '1'), ('b', '0'), ('b', '1')),
                         (('b', '0'), ('b', '1'), ('b', '0'), ('a', '1')),
                         (('b', '0'), ('b', '1'), ('b', '0'), ('b', '1')),
                         ], 2)