open Generator[States, Events]

-- A simple example for checking the Generator module.
-- copyright Richard St-Denis, Universite de Sherbrooke, 2015.

enum States { s0, s1, s2, s3, s4, s5 }
enum Events { a, b, c, d, e }

one sig G extends Generator { }
{
 states = s0 + s1 + s2 + s3 + s4 + s5
 events = a + b + c + d + e
 transition = s0->a->s1 + s1->b->s2 + s2->c->s3 + s3->d->s0 + s3->e->s5
 initialState = s0
 markedStates = s5
 ctrlEvents = a
}

one sig w extends Walk { }
{ -- to check Extension
 edges[0] = a
 edges[1] = b
 edges[2] = c
 edges[3] = d
 edges[4] = a
 walkLength = 5
 stg = G
}


one sig w1 extends Walk { }
{ -- to check Extension
 edges[0] = a
 edges[1] = b
 edges[2] = c
 edges[3] = d
 walkLength = 4
 stg = G
}


run { } for 1 but 5 Int, 15 seq, 2 Walk

check lastStepIsCtrlYes { lastStepIsCtrl[w] } for 1
      but 5 Int, 10 seq, 2 Walk

check lastStepIsCtrlNo { lastStepIsCtrl[w1] } for 1
      but 5 Int, 10 seq, 2 Walk