module DistributedArchitectures[StateSpace, EventSet, DES, Specification]

-- Generator for decentralized architecture.
-- copyright Richard St-Denis, Universite de Sherbrooke, 2015.

-- Reference:
--    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.
--   T.-S. Yoo and S. Lafortune,
--    Decentralized supervisory control with conditional decisions:
--      Supervisor exitence,
--    IEEE Transactions on Automatic Control,
--      49 (11), 1886-1904, 2004.

open Automaton[StateSpace, EventSet, NoInputSymbol] as SPEC

open Generator[StateSpace, EventSet] as SYS


abstract sig NoInputSymbol { }

fact
{
 no NoInputSymbol
 no SPEC/SilentEvents
} 


fact
{ -- consistency between a walk and a transition graph
 SYS/Automaton/Walk.stg = DES
 SPEC/Walk.stg = Specification
}

abstract sig CPGenerator extends SYS/Generator
{
 obsEvents        : set EventSet,
 ctrlEventsE      : set EventSet,  -- controllable events for which
                                   --   the default setting is enablement
 ctrlEventsD      : set EventSet,  -- controllable events for which
                                   --   the default setting is disablement
 nbrOfSupervisors : Int,
 ctrlEventSet     : set Int -> set EventSet,
 obsEventSet      : set Int -> set EventSet
}
{
 obsEvents in events
 ctrlEventsE + ctrlEventsD = ctrlEvents
 ctrlEventsE & ctrlEventsD = none
 (all i : Int |         i >= 1 and i <= nbrOfSupervisors
                implies ctrlEventSet[i] in ctrlEvents)
 (all i : Int |         i >= 1 and i <= nbrOfSupervisors
                implies obsEventSet[i] in obsEvents)
}

pred Observability
{ -- observability property
 all ws1 : SPEC/Walk, w1 : SYS/Automaton/Walk, sigma : DES.ctrlEvents |
        (    ws1.edges = w1.edges
         and not isAnExtension[ws1, sigma]
         and isAnExtension[w1, sigma])
     implies
        (all ws2 : SPEC/Walk |
                  projectWalk[ws2, DES.obsEvents]
                = projectWalk[ws1, DES.obsEvents]
             implies
                not isAnExtension[ws2, sigma])
}

pred CPCoObservability[defaultEnablement : set EventSet]
{ -- C&P co-observability property
 all ws1 : SPEC/Walk, w1 : SYS/Automaton/Walk, sigma : defaultEnablement |
        (    ws1.edges = w1.edges
         and not isAnExtension[ws1, sigma]
         and isAnExtension[w1, sigma])
     implies
        (some i : Int |
                  i <= DES.nbrOfSupervisors
              and sigma in DES.ctrlEventSet[i] & defaultEnablement
              and (all ws2 : SPEC/Walk |
                            projectWalk[ws2, DES.obsEventSet[i]]
                          = projectWalk[ws1, DES.obsEventSet[i]]
                       implies
                          not isAnExtension[ws2, sigma]))
}

pred DACoObservability[defaultDisablement : set EventSet]
{ -- D&A co-observability property
 all ws1 : SPEC/Walk, sigma : defaultDisablement |
           isAnExtension[ws1, sigma]
     implies
        (some i : Int |
                  i <= DES.nbrOfSupervisors
              and sigma in DES.ctrlEventSet[i] & defaultDisablement
              and (all ws2 : SPEC/Walk, w2 : SYS/Automaton/Walk |
                          (    w2.edges = ws2.edges
                           and   projectWalk[ws2,DES.obsEventSet[i]]
                               = projectWalk[ws1,DES.obsEventSet[i]])
                       implies
                          (    isAnExtension[w2, sigma]
                           and isAnExtension[ws2, sigma])))
}

pred CoObservability
{ -- Co-observability property
     CPCoObservability[DES.ctrlEventsE]
 and DACoObservability[DES.ctrlEventsD]
}

pred CCPCoObservability[defaultEnablement : set EventSet]
{ -- conditional C&P co-observability property
 all ws1 : SPEC/Walk, w1 : SYS/Automaton/Walk, sigma : defaultEnablement |
        (    ws1.edges = w1.edges
         and not isAnExtension[ws1, sigma]
         and isAnExtension[w1, sigma])
     implies
        (some i : Int |
                  i <= DES.nbrOfSupervisors
              and sigma in DES.ctrlEventSet[i] & defaultEnablement
              and (all ws2 : SPEC/Walk |
                          (      projectWalk[ws2,DES.obsEventSet[i]]
                               = projectWalk[ws1,DES.obsEventSet[i]]
                           and isAnExtension[ws2, sigma])
                       implies
                          (some j : Int |
                                    j <= DES.nbrOfSupervisors
                                and sigma in DES.ctrlEventSet[j] & defaultEnablement
                                and (all ws3 : SPEC/Walk, w3 : SYS/Automaton/Walk |
                                            (    w3.edges = ws3.edges
                                             and   projectWalk[ws3,DES.obsEventSet[j]]
                                                 = projectWalk[ws2,DES.obsEventSet[j]]
                                             and isAnExtension[w3, sigma])
                                         implies
                                             isAnExtension[ws3, sigma]))))
}

pred CDACoObservability[defaultDisablement : set EventSet]
{ -- conditional D&A co-observability property
 all ws1 : SPEC/Walk, sigma : defaultDisablement |
           isAnExtension[ws1, sigma]
     implies
        (some i : Int |
                  i <= DES.nbrOfSupervisors
              and sigma in DES.ctrlEventSet[i] & defaultDisablement
              and (all ws2 : SPEC/Walk, w2 : SYS/Automaton/Walk |
                          (    w2.edges = ws2.edges
                           and   projectWalk[ws2,DES.obsEventSet[i]]
                               = projectWalk[ws1,DES.obsEventSet[i]]
                           and isAnExtension[w2, sigma]
                           and not isAnExtension[ws2, sigma]) 
                       implies
                          (some j : Int |
                                    j <= DES.nbrOfSupervisors
                                and sigma in DES.ctrlEventSet[j] & defaultDisablement
                                and (all ws3 : SPEC/Walk |
                                              projectWalk[ws3,DES.obsEventSet[j]]
                                            = projectWalk[ws2,DES.obsEventSet[j]]
                                         implies
                                            not isAnExtension[ws3, sigma]))))
}