open DistributedArchitectures[StateSpace, EventSet, G, H] as UDA

-- A simple example for checking observability.
--   T.-S. Yoo and S. Lafortune,
--    Decentralized supervisory control with conditional decisions:
--      Supervisor exitence,
--    IEEE Transactions on Automatic Control,
--      49 (11), 1886-1904, 2004,
--      Proposition 1 with H of Fig. 12.
-- copyright Richard St-Denis, Universite de Sherbrooke, 2015.

enum StateSpace { S1, S2, S3, S4, S5, S6, S7, S8, S9, S10,
                  S11, S12, S13, S14, S15, S16, S17, S18, S19, S20 }
enum EventSet { a, ap, b, bp, c, d }

one sig G extends CPGenerator { }
{
 states = S1 + S2 + S3 + S4 + S5 + S6 + S7 + S8 + S9 + S10
        + S11 + S12 + S13 + S14 + S15 + S16 + S17 + S18 + S19 + S20
 events = a + ap + b + bp + c + d
 transition = S1->b->S2 + S1->c->S3 + S1->a->S4
            + S2->ap->S5 + S2->c->S6
            + S3->d->S11
            + S4->c->S7 + S4->bp->S8
            + S5->c->S9 + S8->c->S10
            + S11->b->S12 + S11->d->S13 + S11->a->S14
            + S12->ap->S15 + S12->d->S16
            + S14->d->S17 + S14->bp->S18
            + S15->d->S19 + S18->d->S20
 initialState = S1
 markedStates = S1 + S2 + S3 + S4 + S5 + S6 + S7 + S8 + S9 + S10
              + S11 + S12 + S13 + S14 + S15 + S16 + S17 + S18 + S19 + S20
 ctrlEvents = c + d
 ctrlEventsE = none  -- none for checking D&A co-observability property
                     -- gamma for checking C&P co-observability property
 obsEvents = none    -- a + ap + b + bp + c + d
 nbrOfSupervisors = 2
 ctrlEventSet[1] = none  -- c + d
 ctrlEventSet[2] = none
 obsEventSet[1] = none   -- a + ap + b + bp + c + d
 obsEventSet[2] = none
}

one sig H extends UDA/SPEC/Automaton { }
{
 states = S1 + S2 + S3 + S4 + S5 + S8 + S9 + S10
        + S11 + S12 + S14 + S15 + S16 + S17 + S18
 labels = a + ap + b + bp + c + d
 transition = S1->b->S2 + S1->c->S3 + S1->a->S4
            + S2->ap->S5
            + S3->d->S11
            + S4->bp->S8
            + S5->c->S9 + S8->c->S10
            + S11->b->S12 + S11->a->S14
            + S12->ap->S15 + S12->d->S16
            + S14->d->S17 + S14->bp->S18
 initialState = S1
 finalStates = S1 + S2 + S3 + S4 + S5 + S8 + S9 + S10
             + S11 + S12 + S14 + S15 + S16 + S17 + S18
}


run { } for 1
    but 5 Int, 10 seq, 3 UDA/SYS/Automaton/Walk
 
check ObservabilityNo { Observability } for 1
      but 5 Int, 7 seq, 2 UDA/SYS/Automaton/Walk,
                         3 UDA/SPEC/Walk

check ObservabilityYes { Observability } for 1  -- obsEvents = a+ap+b+bp+c+d
      but 5 Int, 7 seq, 2 UDA/SYS/Automaton/Walk,
                        3 UDA/SPEC/Walk