module Component[StateSpace, Input, Output, Agent, Interface] -- Definition of a component (hierarchical control). -- copyright Richard St-Denis, Universite de Sherbrooke, 2013. open Automaton[StateSpace, Label, SeqIdx] as A -- Agent + causal map -- (Mealy machine) open Automaton[StateSpace, Output, SeqIdx] as I -- Interface --open util/ordering[SeqIdx] as ORD -- Labels of the Mealy Machine abstract sig Label { Sigma : Input, T : Output } sig SeqIdx {} fact { -- consistency between a walk and a transition graph A/Walk.graph = Agent I/Walk.graph = Interface } fun theta[aw: one A/Walk] : I/Walk { -- causal map let iw = { i : SeqIdx, o : Output | A/ORD/lte[i, A/ORD/max[(aw.edges).Label]] and o = (i.(aw.edges)).T } | { w : I/Walk | w.edges = iw } } fact { -- the causal map is a total function over A/Walk all aw : A/Walk | some iw : I/Walk | theta[aw] = iw } fun eClosure[x : one StateSpace] : Agent.states { Agent.A/GetReachableStates[x, T.SilentEvents] } fun outputFrom[x : one StateSpace] : Output { x.(Agent.transition).StateSpace.T } -- Consistency of marking 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 consistencyOfMarking { -- Consistency of marking all aw : A/Walk | (let v = lastVertex[aw] | theta[aw].IsAccepted iff some Agent.finalStates & eClosure[v]) } -- Observer property -- K.C. Wong and W.M. Wonham, -- Hierarchical control of discrete-event systems, -- Discrete Event Dynamic Systems: Theory and Applications, -- 6 (3), 241-273, 1996. pred observer { -- obsever property -- seq must be longer than 2*#Agent.states + 1 all aw : A/Walk, tau : Output | --(walkLength[aw] <= #Agent.transition (not IsSilent[tau] and (some iw : I/Walk | iw = Extension[theta[aw], tau])) implies (some x2 : Agent.states | let x1 = lastVertex[aw] | x2 in eClosure[x1] and tau in outputFrom[x2]) } -- Condition on the standard control technology for the agent -- D. Cote and R. St-Denis, -- Component-based method for the modeling and control of modular -- production systems, -- IEEE Transactions on Control Systems Technology, 21 (5), 1570-1585, 2013. pred conditionOnSCT { -- condition on the standard control technology for the interface all iw : I/Walk | not iw.lastLabel.IsSilent implies (all aw : A/Walk | -- aw is automatically a vocal A/Walk iw = theta[aw] implies (LastStepIsCtrl[iw] implies LastStepIsCtrl[aw])) }