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 3 with H of Fig. 6.
-- copyright Richard St-Denis, Universite de Sherbrooke, 2015.

enum StateSpace { S1, S2, S3, S4, S5, S6 }
enum EventSet { alpha, beta, gamma }

one sig G extends CPGenerator { }
{
 states = S1 + S2 + S3 + S4 + S5 + S6
 events = alpha + beta + gamma
 transition = S1->gamma->S2 + S1->beta->S3 + S1->alpha->S4
            + S3->gamma->S5 + S4->gamma->S6 
 initialState = S1
 markedStates = S1 + S2 + S3 + S4 + S5 + S6
 ctrlEvents = gamma
 ctrlEventsE = none  -- none for checking D&A co-observability property
                     -- gamma for checking C&P co-observability property
 obsEvents = alpha + beta + gamma
 nbrOfSupervisors = 2
 ctrlEventSet[1] = gamma
 ctrlEventSet[2] = gamma
 obsEventSet[1] = alpha + gamma
 obsEventSet[2] = beta + gamma
}

one sig H extends UDA/SPEC/Automaton { }
{
 states = S1 + S2 + S3 + S4
 labels = alpha + beta + gamma
 transition = S1->gamma->S2 + S1->beta->S3 + S1->alpha->S4
 initialState = S1
 finalStates = S1 + S2 + S3 + S4
}


run { } for 1

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

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