open BasicProperties[StateSpace, EventSet]

-- A simple example for checking the normality property.
-- copyright Richard St-Denis, Universite de Sherbrooke, 2013.

enum StateSpace { S1, S2, S3, S4, 
                  H1, H2, H3, H4, 
                  C1, C2, C3 }
enum EventSet { a ,b, c, d }

one sig G extends CtrlAutomaton { }
{
 states = S1 + S2 + S3 + S4
 events = a + b + c + d
 controllableEvents = none
 transition = S1->a->S2 + S2->b->S4 + S1->c->S3 + S3->d->S4
 initialState = S1
 markedStates = S1 + S2 + S3 + S4
}

one sig H extends CtrlAutomaton { }
{
 states = H1 + H2 + H3 + H4
 events = a + b + c + d
 controllableEvents = none
 transition = H1->a->H2 + H2->b->H4 + H1->c->H3 
         -- + H3->d->H4 -- remove the comment for normality
 initialState = H1
 markedStates = H1 + H2 + H3 + H4
}

fun f: H.states->G.states
{
 H1->S1 + H2->S2 + H3->S3 + H4->S4
}

fun M: EventSet->EventSet
{
 a->a + b->b + c->a + d->b
}

one sig C extends CtrlAutomaton { }
{
 states = C1 + C2 + C3
 events = a + b
 controllableEvents = none
 transition = C1->a->C2 + C2->b->C3
 initialState = C1
 markedStates = C1 + C2 + C3
}

fun r: C.states -> set H.states
{
 C1->H1 + C2->H2 + C2->H3 + C3->H4
}

run { }

check IsGtrimed { IsTrim[G] }
check IsHtrimed { IsTrim[H] }
check IsCtrimed { IsTrim[C] }
check IsHnormal { normality[G, H, C, f, M, r] }