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

-- A simple example for checking C&P and D&A coobservability.
--   T.-S. Yoo and S. Lafortune,
--    A general architecture for decentralized supervisory control
--      of dicrete-event systems,
--    Discrete Event Dynamic Systems: Theory and Applications,
--      12 (3), 335-377, 2002,
--      Proposition 4 with H of Fig. 8b.
-- copyright Richard St-Denis, Universite de Sherbrooke, 2015.

enum StateSpace { S1, S2, S3, S4, S5, S6, S7, S8, S9, S10, S11 }
enum EventSet { alpha, beta, gamma, delta }

one sig G extends CPGenerator { }
{
 states = S1 + S2 + S3 + S4 + S5 + S6 + S7 + S8 + S9 + S10 + S11
 events = alpha + beta + gamma + delta
 transition = S1->gamma->S2 + S1->beta->S3 + S1->alpha->S4
            + S3->gamma->S5 + S4->gamma->S6
            + S5->delta->S7 + S5->beta->S8 + S5->alpha->S9
            + S8->delta->S10 + S9->delta->S11
 initialState = S1
 markedStates = S1 + S2 + S3 + S4 + S5 + S6 + S7 + S8 + S9 + S10 + S11
 ctrlEvents = gamma + delta
 ctrlEventsE = delta
 ctrlEventsD = gamma  -- unnecessary because facts 
 obsEvents = alpha + beta + gamma + delta
 nbrOfSupervisors = 2
 ctrlEventSet[1] = gamma + delta
 ctrlEventSet[2] = gamma + delta
 obsEventSet[1] = alpha + gamma + delta
 obsEventSet[2] = beta + gamma + delta
}

one sig H extends UDA/SPEC/Automaton { }
{
 states = S1 + S3 + S4 + S5 + S6 + S7 + S8 + S9
 labels = alpha + beta + gamma + delta
 transition = S1->beta->S3 + S1->alpha->S4
            + S3->gamma->S5 + S4->gamma->S6
            + S5->delta->S7 + S5->beta->S8 + S5->alpha->S9
 initialState = S1
 finalStates = S1 + S3 + S4 + S5 + S6 + S7 + S8 + S9
}


check CPCoObservabilityNo { CPCoObservability[gamma + delta] } for 1
     but 6 Int, 15 seq, 2 UDA/SYS/Automaton/Walk,
                        3 UDA/SPEC/Walk

check DACoObservabilityNo { DACoObservability[gamma + delta] } for 1
     but 6 Int, 15 seq, 2 UDA/SYS/Automaton/Walk,
                        3 UDA/SPEC/Walk

check CPCoObservabilityYes { CPCoObservability[delta] } for 1
     but 6 Int, 15 seq, 2 UDA/SYS/Automaton/Walk,
                        3 UDA/SPEC/Walk

check DACoObservabilityYes { DACoObservability[gamma] } for 1
     but 6 Int, 15 seq, 2 UDA/SYS/Automaton/Walk,
                        3 UDA/SPEC/Walk

check CoObservabilityYes { CoObservability } for 1
     but 6 Int, 15 seq, 2 UDA/SYS/Automaton/Walk,
                        3 UDA/SPEC/Walk