-- ========================================================================
--                    extended states with data
-- ========================================================================

-- ========================================================================
require pnat
require genCases
require predCj

-- ========================================================================
-- state and data
mod* ST-DT {ex(PNAT)
[Ste Data] ops p q : Ste Data -> Bool . op m : Ste Data -> Nat.PNAT .
[Pnm < PnmSeq] op cj : PnmSeq Ste -> Bool .
}
-- ========================================================================
-- extended states with data
mod! EX-STATE (SD :: ST-DT) {inc(RWL) ex(GENcases)
[ExState Infom] 
-- state constructor for extended states
op _%_ : Ste Data -> ExState {constr}
-- the transitions on ExState is the same as the transitons on Ste
eq ((S:Ste % D:Data) =(*,1)=>+ (SS:Ste % D)
        if CC:Bool suchThat B:Bool {I:Infom}) 
    = (S =(*,1)=>+ SS if CC suchThat B {I}) .
eq ((S:Ste % D:Data) =(*,1)=>+ (SS:Ste % D)) = (S =(*,1)=>+ SS) .
-- predicates p and q on ExState
ops p q : ExState -> Bool .
eq p(S:Ste % D:Data) = p(S,D) .
eq q(S:Ste % D:Data) = q(S,D) .
-- measure function on ExState
op m : ExState -> Nat.PNAT .
eq m(S:Ste % D:Data) = m(S,D) .
-- 
-- t__  is introduced in the module GENcases
[Ste Data ExState < Val]
eq t("_%_")(S:Ste,D:Data) = (S % D) .
}

-- ========================================================================
mod! PCJ-EX-STATE (SD :: ST-DT) {
ex((PREDcj((EX-STATE(SD)){sort Elt -> ExState}))
    *{sort Pname -> ExPname, sort PnameSeq -> ExPnameSeq})
[Pnm < ExPname] [PnmSeq < ExPnameSeq] 
eq cj(PN:Pnm,(S:Ste % D:Data)) = cj(PN,S) .
}

-- ========================================================================
provide exState

-- ========================================================================
eof
** end of file