Maude-help mailing list

[Julia Sapiña Sanchis <jsapina AT upv.es>]

Hi Pierce,

I've noticed a few errors in your example:

subclass MultiInPort < InPort
->
subclass MultiInPort < InPort .

subsort connection < ObjectConfiguration .
->
subsort Connection < ObjectConfiguration .

subclass timedPlotter < TimeActor .
->
subclass TimedPlotter < TimeActor .

op _!_ : ActorID PortId -> EPortId [ctor] .
->
op _!_ : ActorID PortID -> EPortId [ctor] .

vars P P' : PortId .
->
vars P P' : PortID .

Also, sorts Time ObjectConfiguration Value ActorID Exp AssignMap 
NEConfiguration NzTime VarId are not declared.

Actually, I've only peeked half of the code, mostly operators, 
sorts/subsorts, and classes/subclasses declarations but no rules or 
equations, so I guess there are a lot more errors to discover. Maybe 
reordering your code may help find them faster.

Regards,

Julia

El 26/06/2019 a las 0:51, 
pdouglis AT perspectalabs.com
 escribió:
> 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.