open Component[StateSpace, Input, Output, Agent, Interface] as C -- A simple example for checking the observer property inspired from: -- 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. -- copyright Richard St-Denis, Universite de Sherbrooke, 2013. enum StateSpace {x0, x1, x2, x3, x4, x5, x6, y0, y1, y2, y3} enum Input {alpha, beta, delta, gamma} enum Output {tau, tau1,tau2, epsilon} fact { -- hidden events in module A (agent) and I (interface) no C/A/SilentEvents epsilon = C/I/SilentEvents } one sig l0, l1, l2, l3, l4 extends C/Label { } fact { -- Theta Sigma = l0->alpha + l1->alpha + l2->beta + l3->gamma + l4->delta T = l0->tau + l1->epsilon + l2->epsilon + l3->tau1 + l4->tau2 -- + l4->tau1 -- (replace last entry for observer) } one sig Agent extends C/A/CtrlAutomaton { } { states = x0 + x1 + x2 + x3 + x4 + x5 + x6 labels = l0 + l1 + l2 + l3 + l4 controllableEvents = l3 transition = x0->l0->x1 + x1->l1->x2 + x1->l2->x3 + x2->l1->x4 + x4->l3->x5 + x3->l4->x6 initialState = x0 finalStates = x5 + x6 -- remove x6 to violate the consistency of marking } one sig Interface extends C/I/CtrlAutomaton { } { states = y0 + y1 + y2 + y3 labels = tau + tau1 + tau2 controllableEvents = tau1 -- + tau2 -- remove the comment to violate the condition on SCT transition = y0->tau->y1 + y1->tau1->y2 + y1->tau2->y3 -- + y1->tau1->y3 -- (replace last entry for observer) initialState = y0 finalStates = y2 + y3 } run { } for 1 but 10 SeqIdx, 1 C/A/Walk, 1 C/I/Walk check consistencyOfMarking {C/consistencyOfMarking} for 1 but 10 SeqIdx, 1 C/A/Walk, 1 C/I/Walk check observer {C/observer} for 1 but 10 SeqIdx, 1 C/A/Walk, 2 C/I/Walk check conditionOnSCT {C/conditionOnSCT} for 1 but 10 SeqIdx, 1 C/A/Walk, 1 C/I/Walk