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. 17.
-- copyright Richard St-Denis, Universite de Sherbrooke, 2014.

enum StateSpace { S1, S2, S3, S4, S5, S6, S7, S8 }
enum EventSet { i1, i2, o1, o2, s, p }

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

one sig H extends UDA/SPEC/Automaton { }
{
 states = S1 + S2 + S3 + S4 + S5
 labels = i1 + i2 + o1 + o2 + s + p
 transition = S1->i1->S2 + S1->i2->S3 + S1->p->S1
            + S2->o2->S4 + S2->s->S2
            + S3->o1->S5 + S3->s->S3
            + S4->p->S1
            + S5->p->S1
 initialState = S1
 finalStates = S1 + S2 + S3 + S4 + S5
}


run { } for 1
    but 5 Int, 10 seq, 3 UDA/SYS/Automaton/Walk
 
check CPCoObservabilityNo { CCPCoObservability[s+p] } for 1
      but 4 Int, 7 seq, 3 UDA/SYS/Automaton/Walk,
                         5 UDA/SPEC/Walk
         

check CDACoObservabilityNo { CDACoObservability[s+p] } for 1
      but 4 Int, 7 seq, 3 UDA/SYS/Automaton/Walk,
                        5 UDA/SPEC/Walk

check CPCoObservabilityYes { CCPCoObservability[p] } for 1
      but 4 Int, 7 seq, 3 UDA/SYS/Automaton/Walk,
                        5 UDA/SPEC/Walk
         

check CDACoObservabilityYes { CDACoObservability[s] } for 1
      but 4 Int, 7 seq, 3 UDA/SYS/Automaton/Walk,
                        5 UDA/SPEC/Walk