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 5 with H of Fig. 11b. -- 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 } one sig G extends CPGenerator { } { states = S1 + S2 + S3 + S4 + S5 + S6 + S7 + S8 + S9 + S10 + S11 events = alpha + beta + gamma transition = S1->gamma->S2 + S1->beta->S3 + S1->alpha->S4 + S3->gamma->S5 + S4->gamma->S6 + S5->gamma->S7 + S5->beta->S8 + S5->alpha->S9 + S8->gamma->S10 + S9->gamma->S11 initialState = S1 markedStates = S1 + S2 + S3 + S4 + S5 + S6 + S7 + S8 + S9 + S10 + S11 ctrlEvents = gamma ctrlEventsE = none 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 + S3 + S4 + S5 + S6 + S7 + S8 + S9 labels = alpha + beta + gamma transition = S1->beta->S3 + S1->alpha->S4 + S3->gamma->S5 + S4->gamma->S6 + S5->gamma->S7 + S5->beta->S8 + S5->alpha->S9 initialState = S1 finalStates = S1 + S3 + S4 + S5 + S6 + S7 + S8 + S9 } check CPCoObservabilityNo { 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 check ObservabilityYes { Observability } for 1 but 6 Int, 15 seq, 2 UDA/SYS/Automaton/Walk, 3 UDA/SPEC/Walk