Maude-help mailing list

[Francisco Durán <duran AT lcc.uma.es>]

Alberto,

Can you please answer Abdur.

Thanks,

Paco


El 10/06/2009, a las 13:16, 
rza AT Cs.Nott.AC.UK
 escribió:

> Hi all,
>
> Could you please let me know, if maude strategy language described  
> in http://maude.sip.ucm.es/strategies/index.html work together with  
> LTL model checking? I observe that using full maude the LTL model  
> checking works fine, also the strategy language described above  
> works fine(according to the direction given there). However, when I  
> am using them together it does't work:
>
> My error log is shown below (TREE is module, TREE-PRED is another  
> module where model checking stuff is defined using "pr TREE .", and  
> TREE-STRAT is strategy module, detailed can be found in the attached  
> file) :
>
>
> [rza@goldfinger
>  model-tree]$ /home/rza/MAUDE/maude-linux/maude.linux
>                    \||||||||||||||||||/
>                  --- Welcome to Maude ---
>                    /||||||||||||||||||\
>           Maude 2.4 built: Nov  6 2008 17:14:50
>           Copyright 1997-2008 SRI International
>                  Wed Jun 10 11:40:49 2009
> Maude> load maude-strat.maude
>
>      Full Maude 2.3 `(February 12th`, 2007`)
>
> rewrites: 53 in 3ms cpu (3ms real) (17666 rewrites/second)
>
>              Maude Strategy Language 2.5 (December 2nd, 2007)
>
> Maude> load model-checker.maude
> Maude> select FULL-MAUDE .
> Maude> loop init .
> rewrites: 150 in 3ms cpu (4ms real) (37509 rewrites/second)
>
>      Full Maude 2.3 `(February 12th`, 2007`)
>
> Maude> load tree-full-st.maude
> rewrites: 5515 in 42ms cpu (42ms real) (128276 rewrites/second)
> Introduced module TREE
>
> rewrites: 3998 in 29ms cpu (30ms real) (133284 rewrites/second)
> Introduced module TREE-PRED
>
> rewrites: 11 in 2ms cpu (3ms real) (3667 rewrites/second)
> Warning: Parse error in smod <---*HERE*
> Error: No parse for input.
>
> Regds,
> --Abdur
>
> This message has been checked for viruses but the contents of an  
> attachment
> may still contain software viruses, which could damage your computer  
> system:
> you are advised to perform your own checks. Email communications  
> with the
> University of Nottingham may be monitored as permitted by UK  
> legislation.
>
> <tree-full-st.maude>_______________________________________________
> Maude-help mailing list
> Maude-help AT maude.cs.uiuc.edu
> http://maude.cs.uiuc.edu/cgi-bin/mailman/listinfo/maude-help