Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

On Wednesday 28 July 2004 01:44 pm, 
yfu002 AT cs.fiu.edu
 wrote:
> Dear Maude supporters,
>
> I am using Core Maude 2.1. I define tokens for first order linear time
> temporal logic, which is shown in attached file. When I try to reduce a
> first order LTL formula, I get nothing. This is shown in the attached .gif
> file. Would you please take a look at that file? Thanks in advance.
>
>
> --Yujian Fu

There are a number of problems; first

  eq D ( E ) : D{E} .
  eq E ( true )  : E{true} .
  eq E ( false ) : E{false} .

in fmod FOLTL do not have = symbols so Maude does not recgnized the end of 
equations or the end of the module.

Next the term

V- green : [] ( D ( green ) /\ E ( true ) -> <> ( d ( green ) \/ t ( false ) 
)) .

makes use of green which is declared to be a variable in another module (not 
the current one) and t which appears to be an undeclared operator.

Steven