open DistributedArchitectures[StateSpace, EventSet, G, H] as UDA -- A simple example for checking conditional C&P and D&A coobservability. -- T.-S. Yoo and S. Lafortune, -- Decentralized supervisory control with conditional decisions: -- Supervisor exitence, -- IEEE Transactions on Automatic Control, -- 49 (11), 1886-1904, 2004, -- Theorem 2 with H of Fig. 7. -- copyright Richard St-Denis, Universite de Sherbrooke, 2015. enum StateSpace { S1, S2, S3, S4, S5, S6, S7, S8, S9, S10 } enum EventSet { a, ap, b, bp, c } one sig G extends CPGenerator { } { states = S1 + S2 + S3 + S4 + S5 + S6 + S7 + S8 + S9 + S10 events = a + ap + b + bp + c transition = S1->b->S2 + S1->c->S3 + S1->a->S4 + S2->ap->S5 + S2->c->S6 + S4->c->S7 + S4->bp->S8 + S5->c->S9 + S8->c->S10 initialState = S1 markedStates = S1 + S2 + S3 + S4 + S5 + S6 + S7 + S8 + S9 + S10 ctrlEvents = c ctrlEventsE = none -- none for checking D&A co-observability property -- gamma for checking C&P co-observability property obsEvents = a + ap + b + bp + c nbrOfSupervisors = 2 ctrlEventSet[1] = c ctrlEventSet[2] = c obsEventSet[1] = a + ap + c obsEventSet[2] = b + bp + c } one sig H extends UDA/SPEC/Automaton { } { states = S1 + S2 + S4 + S5 + S6 + S7 + S8 labels = a + ap + b + bp + c transition = S1->b->S2 + S1->a->S4 + S2->ap->S5 + S2->c->S6 + S4->c->S7 + S4->bp->S8 initialState = S1 finalStates = S1 + S2 + S4 + S5 + S6 + S7 + S8 } run { } for 1 but 5 Int, 10 seq, 3 UDA/SYS/Automaton/Walk check CPCoObservabilityNo { CCPCoObservability[c] } for 1 but 4 Int, 7 seq, 3 UDA/SYS/Automaton/Walk, 5 UDA/SPEC/Walk check CDACoObservabilityYes { CDACoObservability[c] } for 1 but 4 Int, 7 seq, 3 UDA/SYS/Automaton/Walk, 5 UDA/SPEC/Walk