Maude-help mailing list

[<pdouglis AT perspectalabs.com>]

Dear Stephen,
Thank you for the quick reply. I saw no way to attach the file, but I'll paste
its text below:

(omod PTOLEMY is
    protecting QID .
    class Actor | ports : Configuration, parameters : Configuration .
    sort ParamID .
    subsort Qid < ParamID < Oid .
    class Parameter | value : Value .
    class TimeActor | currentTime : Time .
    subclass TimeActor < Actor .
    class Clock | index : Nat .
    subclass Clock < Actor .
    class CurrentTime .
    subclass CurrentTime < TimeActor .
    class TimedPlotter | eventHistory : EventHistory .
    subclass timedPlotter < TimeActor .
    sorts EventTriple EventHistory .
    subsort EventTriple < EventHistory .
    op source:_time:_value:_ : EPortId Time Value -> EventTriple [ctor] .
    op emptyHistory : -> EventHistory [ctor] .
    op _++_ : EventHistory EventHistory -> EventHistory [ctor assoc id:
emptyHistory] .
    class Delay .
    class VariableDelay .
    class Timer .
    class Pulse | index : Nat .
    subclass Delay VariableDelay Timer Pulse < Actor .
    class NonInterruptibleTimer | processing : Bool, waitQueue : TimeList .
    subclass NonInterruptibleTimer < Actor .

    sort TimeList .
    subsort Time < TimeList .
    op emptyList : -> TimeList [ctor] .
    op __ : TimeList TimeList -> TimeList [ctor assoc id: emptyList] .

    class FSM-Actor | currState : Location, initState : Location,
transitions : TransitionSet .
    subclass FSM-Actor < Actor .
    sort Location .
    subsort Qid < Location .
    sorts Transition TransitionSet .
    subsort Transition < TransitionSet .
    op _-->_'{_'} : Location Location TransBody -> Transition [ctor] .
    op emptyTransitionSet : -> TransitionSet [ctor] .
    op _;_ : TransitionSet TransitionSet -> TransitionSet [ctor assoc comm id:
emptyTransitionSet] .
    sort TransBody .
    op guard:_output:_set:_ : Exp AssignMap AssignMap -> TransBody [ctor] .

    sort PortID .
    subsort Qid < PortID < Oid .
    class Port | status : PortStatus, value : Value .
    class InPort .
    subclass InPort < Port .
    class OutPort .
    subclass OutPort < Port .
    sort PortStatus .
    ops unknown present absent : -> PortStatus [ctor] .
    class MultiInPort | source : EPortIdSet .
    subclass MultiInPort < InPort

    sort Connection .
    op _==>_ : EPortId EPortIdSet -> Connection [ctor] .
    subsort connection < ObjectConfiguration .
    sort EPortId .
    op _!_ : ActorID PortId -> EPortId [ctor] .
    sort EPortIdSet .
    subsort EPortId < EPortIdSet .
    op noPort : -> EPortIdSet [ctor] .
    op _;_ : EPortIdSet EPortIdSet -> EPortIdSet [ctor assoc comm id:
noPort] .

    sort Event .
    op event : EPortId Value -> Event [ctor] .
    sort Events .
    subsort Event < Events .
    op noEvent : -> Events [ctor] .
    op __ : Events Events -> Events [ctor assoc comm id: noEvent] .
    sort TimedEvent .
    op _;_;_ : Events Time Nat -> TimedEvent [ctor] .
    sort EventQueue .
    subsort TimedEvent < EventQueue .
    op nil : -> EventQueue [ctor] .
    op _::_ : EventQueue EventQueue -> EventQueue [ctor assoc id: nil] .

    var CF : Configuration .
    vars NECF NECF' : NEConfiguration .
    vars OBJ OBJECT : Object .
    vars SYSTEM OBJECTS REST PORTS PORTS2 PARAMS : ObjectConfiguration
    vars O O' : Oid .
    vars P P' : PortId .
    vars EPIS EPIS' : EPortIdSet .
    var PS : PortStatus .
    var VI : VarId .
    vars V V1 V2 TV : Value .
    vars E TG : Exp .
    var EVTS : Events .
    vars STATE STATE' : Location .
    var QUEUE : EventQueue .
    var EH : EventHistory .
    var T T' : Time .
    var NZT : NzTime .
    var N : Nat .
    var NZ : NzNat .
    var TRANSSET : TransitionSet .
    var BODY : TransBody .
    vars OL AL : AssignMap .

    rl [tick] :
       {SYSTEM  < global : EventQueue | queue : (EVTS ; NZT ; N) :: QUEUE >}
      =>
       {delta(SYSTEM, NZT)
        < global : EventQueue | queue : (EVTS ; 0 ; N) :: delta(QUEUE, NZT) >}
       in time NZT .

    op delta : EventQueue Time -> EventQueue .
    eq delta((EVTS ; T ; N) :: QUEUE, T') = (EVTS ; T monus T' ; N) ::
delta(QUEUE, T') .
    eq delta(nil, T) = nil .
    op delta : Configuration Time -> Configuration .
    eq delta(< O : TimeActor | currentTime : T >  REST, T')
     = < O : TimeActor | currentTime : T + T' >  delta(REST, T') .
    eq delta(CF, T) = CF [owise] .
    rl [shortTick] :
       {SYSTEM  < global : EventQueue | queue : (EVTS ; O ; NZ) :: QUEUE >}
      =>
       {SYSTEM  < global : EventQueue | queue : (EVTS ; 0 ; 0) :: QUEUE >} .
    rl [executeStep] :
       {SYSTEM < global : EventQueue | queue : (EVTS ; O ; O) :: QUEUE >}
      =>
       {< global : EventQueue | queue : QUEUE >
        postfire(portFixPoints(addEventsToPorts(EVTS, clearPorts(SYSTEM))))} .
    ops clearPorts portFixPoints postfire : Configuration ~> Configuration .
    eq clearPorts(OBJ CF) = clearPorts(OBJ) clearPorts(CF) .
    eq clearPorts(< O : Actor | ports : PORTS >) = < O : Actor | ports :
clearPorts(PORTS) > .
    eq clearPorts(< P : Port | status : PS > PORTS) = < P : Port | status :
unknown > clearPorts(PORTS) .
    eq clearPorts(CF) = CF [owise] .

    ceq portFixPoints(< O : Actor | ports : < P : OutPort | status : PS,
value : V > PORTS >
                      ((O ! P) ==> ((O' ! P') ; EPIS))
                      < O' : Actor | ports : < P' : InPort | status : unknown
> PORTS2 >
                      REST)
      = portFixPoints(< O : Actor | >
                      ((O ! P) ==> ((O' ! P') ; EPIS))
                      < O' : Actor | ports : < P' : InPort | status : PS,
value : V > PORTS2 >
                      REST)
       if PS =/= unknown .
    ceq portFixPoints(< O : Actor | ports : < P : OutPort | status : unknown >
PORTS >  REST)
      = portFixPoints(< O : Actor | ports : < P : OutPort | status : absent >
                                            setUnknownOutPortsAbsent(PORTS) >
REST)
      if allInputPortsAbsent(PORTS) .
    op allInputPortsAbsent : Configuration -> Bool .
    eq allInputPortsAbsent(< P : InPort | status : PS > PORTS)
      = (PS == absent) and allInputPortsAbsent(PORTS) .
    eq allInputPortsAbsent(PORTS) = true [owise] .
    op setUnknownOutPortsAbsent : Configuration ~> Configuration .
    eq setUnknownOutPortsAbsent(< P : OutPort | status : unknown >  PORTS)
     = < P : OutPort | status : absent >  setUnknownOutPortsAbsent(PORTS) .
    eq setUnknownOutPortsAbsent(PORTS) = PORTS [owise] .
    ceq portFixPoints(< O : Actor | ports : < P : InPort | status : unknown >
PORTS >  REST)
      = portFixPoints(< O : Actor | ports : < P : InPort | status : absent >
PORTS >  REST)
      if not connectedInPort(O ! P, REST) .
    op connectedInPort : EPortId Configuration -> Bool .
    eq connectedInPort(O ! P,  (O' ! P' ==> (O ! P) ; EPIS)  < O' : Actor | >
CF) = true .
    eq connectedInPort(O ! P, CF) = false [owise] .
    eq portFixPoints(< O : Delay | ports : < P : OutPort | status : unknown >
PORTS >  REST)
     = portFixPoints(< O : Delay | ports : < P : OutPort | status : absent >
PORTS >  REST) .
    ceq portFixPoints(< O : CurrentTime | currentTime : T,
                                          ports : < P : InPort | status : PS >
                                                  < P' : OutPort | status :
unknown > >
                      REST)
      = portFixPoints(< O : CurrentTime | ports : < P : InPort | >
                                                  < P' : OutPort | status :
PS, value : # T >
                      REST)
      if PS =/= unknown .
    eq portFixPoints(< O : Pulse | index : N,
                                   parameters : < 'indexes : Parameter |
value : V1 >
                                                < 'values : Parameter |
value : V2 > PARAMS,
                                   ports : < 'trigger : InPort | status :
present >
                                           < 'output : OutPort | status :
unknown > PORTS >
                     REST)
      = portfixPoints(< O : Pulse | ports : < 'trigger : InPort | >
                                            < 'output : OutPort | status :
present,
                                                                  value :
getValue(V1, V2, N) >
                                            PORTS >
                      REST) .
    eq portFixPoints(< O : FSM-Actor | ports : < P' : InPort | status :
present >
                                               < P : OutPort | status :
unknown > PORTS,
                                       currState : STATE,  parameters :
PARAMS,
                                       transitions : (STATE --> STATE' {guard:
TG output : OL set: AL}) ;
                                                      TRANSSET >
                     REST)
      = portfixPoints(< O : FSM-Actor | ports : < P' : InPort | >
                                                updateOutPorts(PARAMS, OL, <
P : OutPort | > PORTS) >
                      REST)
      if transApplicable(< P' : InPort | > < P : OutPort | > PORTS, PARAMS,
TG) .
    op transApplicable : InPort OutPort ObjectConfiguration
ObjectConfiguration Exp -> Bool .
    eq transApplicable(< P' : InPort | > < P : OutPort | > PORTS, PARAMS, TG)
= (TG == true) .
    op updateOutPorts : Configuration AssignMap Configuration ->
Configuration .
    eq updateOutPorts(PARAMS,  (VI |-> V ; OL), < VI : OutPort | status :
unknown > PORTS)
     = < VI : OutPort | status : present, value : V >  updateOutPorts(PARAMS,
OL, PORTS) .
    eq updateOutPorts(PARAMS, OL, PORTS) = setUnknownOutPortsAbsent(PORTS)
[owise] .
    ceq portfixPoints(< O : FSM-Actor | ports : < P : InPort | status :
present > PORTS,
                                        currState : STATE,  parameters :
PARAMS,  transitions : TRANSSET >
                      REST)
      = portFixPoints(< O : FSM-Actor | ports : < P : InPort | >
setUnknownOutPortsAbsent(PORTS) >
                      REST)
      if allGuardsFalse(STATE, < P : InPort | > PORTS, PARAMS, TRANSSET) .
    eq postfire(OBJECT NECF) = postfire(OBJECT) (postfire NECF) .
    eq postfire(CF) = CF [owise] .
    eq postfire(< O : Delay | ports : < ’input : InPort | status : present,
value : V >
                                      < ’output : OutPort | >,
                              parameters : < ’delay : Parameter | value : TV >
PARAMS >)
       < global : EventQueue | queue : QUEUE >
     =
       < O : Delay | >
       < global : EventQueue | queue : addEvent(event(O ! ’output, V),
toTime(TV),
                                                if toTime(TV) == 0 then 1 else
0 fi, QUEUE) > .
    eq postfire(< O : VariableDelay | ports : < ’input : InPort | status :
present, value : V >
                                              < ’delay : InPort | status :
present, value : TV >
                                              < ’output : OutPort | > PORTS >)
      = < O : VariableDelay | >
        < global : EventQueue | queue : addEvent(event(O ! ’output, V),
toTime(TV),
                                                 if toTime(TV) == 0 then 1
else 0 fi, QUEUE) > .
    ceq postfire(< O : Clock | ports : < P : OutPort | status : present >
PORTS,
                               parameters : < ’offsets : Parameter | value :
V1 >
                                            < ’values : Parameter | value : V2
> PARAMS,
                               index : N >)
        < global : EventQueue | queue : QUEUE >
      =
        < O : Clock | index : N + 1 >
        < global : EventQueue | queue : addEvent(event(O ! P, V2(#(s N))),
TIME-TO-FIRE,
                                                 if TIME-TO-FIRE == 0 then 1
else 0 fi, QUEUE) >
      if TIME-TO-FIRE := toTime((V1(#(s N))) - (V1(# N)))
         /\ ((# N + # 1) lessThan (V1 .. ’length(()) )) == # true .
    eq postfire(< O : Timer | parameters : < ’output : Parameter | value : V >
PARAMS,
                              ports : < ’input : InPort | status : present ,
value : TV > PORTS >)
       < global : EventQueue | queue : QUEUE >
      =
       < O : Timer | >
       < global : EventQueue | queue : addEvent(event(O ! ’output, V),
toTime(TV),
                                                      if toTime(TV) == 0 then
1 else 0 fi, QUEUE) > .
    eq postfire(< O : TimedPlotter | currentTime : T, eventHistory : EH,
ports : PORTS >)
     = < O : TimedPlotter | eventHistory : EH ++ genEventHistory(T, PORTS) > .
    op genEventHistory : Time Configuration ~> EventHistory .
    eq genEventHistory(T, < ’input # (O ! P) : InPort | status : present,
value : V > PORTS)
     = (source: O ! P time: T value: V) ++ genEventHistory(T, PORTS) .
    eq genEventHistory(T, PORTS) = emptyHistory [owise] .
    ceq postfire(< O : FSM-Actor | ports : < P : InPort | status : present >
PORTS,
                                   parameters : PARAMS, currState : STATE,
                                   transitions : STATE --> STATE’ {guard: TG
output: OL set: AL} ;
                                                 TRANSSET >)
      =
         < O : FSM-Actor | parameters : updateParam(PARAMS, AL, PARAMS),
currState : STATE’ >
     if transApplicable(< P : InPort | > PORTS, PARAMS, TG) .
    op updateParam : Configuration AssignMap Configuration -> Configuration .
    eq updateParam(CF, (VI |-> E ; AL), < VI : Parameter | > PARAMS)
     = < VI : Parameter | value : [[ E ]] CF > updateParam(CF, AL, PARAMS) .
    eq updateParam(CF, AL, PARAMS) = PARAMS [owise] .
    eq init(< O : Clock | parameters : < ’value : Parameter | value : V1 >
                                       < ’offsets : Parameter | value : V2 >
PARAMS >
            < global : EventQueue | queue : QUEUE > REST)
     =
       < O : Clock | >
       init(< global : EventQueue | queue : addEvent(event(O ! ’output, V1(#
0)), toTime(V2(# 0)), 0, QUEUE) >
            REST) .
    eq init(CF) = CF [owise] .
endom)

After the "endom", I see
"<---*HERE*
Error: No parse for input." when I try to load the module.


Thank you again for your help,
Pierce

P.S. If this seems at all familiar to anyone, it's from an existing research
paper by Kyungmin Bae et al. I've been trying to piece together its code
snippets with no prior experience with Maude, so anything not explicit in the
paper or in my two days spent with the manual probably went over my head.