module BasicProperties[StateSpace, EventSet]

-- Language-based formulation of basic properties.
-- copyright Richard St-Denis, Universite de Sherbrooke, 2013.

open Automaton[StateSpace, EventSet, SeqIdx]

sig SeqIdx {}

-- Controllability property
--    W.M. Wonham and P.J. Ramadge,
--    On the supremal controllable sublanguage of a given language,
--    SIAM Journal on Control and Optimization, 25 (3), 637-659, 1987.

pred controllability[G, H: one CtrlAutomaton, f: StateSpace->StateSpace]
{
 all y1 : H.states, x1,x2 : G.states, sigma : G.events |
     (    sigma not in G.controllableEvents
      and x1->sigma->x2 in G.transition
      and y1->x1 in f)
 implies
     (some y2 : H.states | y1->sigma->y2 in H.transition)
}

-- Normality property
--    M. Barbeau, G. Custeau, and R. St-Denis,
--    An algorithm for computing the mask value of the supremal normal
--       sublanguage of a legal language,
--    IEEE Transactions on Automatic Control, 40 (4), 699-703, 1995.

pred normality[G, H, C: one CtrlAutomaton, f: StateSpace->StateSpace,
               M: EventSet->EventSet, r: StateSpace->StateSpace]
{
 all y1 : H.states, z1,z2 : C.states, lambda : C.events, sigma : G.events |
     (    (z1->lambda->z2 in C.transition and z1->y1 in r and M[sigma] = lambda)
      and (some x1, x2: G.states |     y1->x1 in f
                                   and x1->sigma->x2 in G.transition))
 implies
     (some y2 : H.states | y1->sigma->y2 in H.transition)
}