Maude-help mailing list

["Skeirik, Stephen R" <skeirik2 AT illinois.edu>]

Dear Pierce,

This file won't load without the dependency `FULL-MAUDE` which specifies the 
grammar of `omods`. You should have a copy of the `FULL-MAUDE` module 
somewhere that you are loading before you load this. If you don't have it, 
you need to get it. There are different versions of available; use the one 
that came with the distribution if possible. Aside from that, you mentioned 
this was from a research paper. Did you copy this module out of a PDF? That 
process is fraught with error and I don't recommend it if you can avoid it 
since certain symbols can get messed up in the PDF conversion process. If you 
can find a source file, please do so. Additionally, if the source archive 
came with a Maude binary, use that one; the Maude parser is fairly consistent 
between versions, but if I recall correctly, the parser was updated somewhat 
in a recent release.

Finally, I would love to help debug this module if I had the time, but it was 
a bit bigger than I was imagining. If you have done all of the above that you 
can and are still stuck, I recommend commenting out the inside of the module 
from end till the beginning and progressively uncommenting declarations until 
you find the first declaration that fails to parse. Then you can fix it and 
move on to the next one.

A general trick is to use parentheses liberally to force your desired parse 
in case of ambiguities (which are more common when using `FULL-MAUDE` based 
tools). Once you have narrowed down where the parse error is, add extra 
parentheses for disambiguation.

Regards,
Stephen

-----Original Message-----
From: 
pdouglis AT perspectalabs.com
 
<pdouglis AT perspectalabs.com>
 
Sent: Tuesday, June 25, 2019 5:51 PM
To: 
maude-help AT lists.cs.illinois.edu;
 Skeirik, Stephen R 
<skeirik2 AT illinois.edu>
Subject: Re: RE: [[Maude-help] ] "No parse for input" after end of module

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.