Maude-help mailing list

[Mihai Gabriel Glont <mihai.glont AT gmail.com>]

Hello,


I am new to Maude and the question I am about to ask will reflect my status. But before I say anything else, I must admit that Maude seems to be a very powerful language, and I'm looking forward to version 2.5 . 

I am student doing his dissertation project in Maude, which entails developing a framework that enables one to encode a biology-inspired computational model into executable Maude specifications. A model contains a multiset(formally, a set where objects need not be unique) of objects, called a soup and a finite set of evolution rules that govern the behaviour of the model.  
Consider the following ebnf notation:
R ::= S Arrow S [Cond], 
Arrow ::= ->, 
S ::= a..z | empty| LSB S RSB, 
LSB ::= [, RSB ::= ], 
Cond ::= Pipe ConditionSet, 
Pipe ::= |, 
ConditionSet ::= Activ | Inh | Activ Comma Inh, 
Comma ::= ',' ,
Activ ::= LB Plus Comma S RB, 
LB ::=(, Plus ::= +, RB ::= ), 
Inh ::= LB Minus, Comma S RB, 
Minus ::= - . 

in which
S is a Soup and R is a rule of type MRule.
Given the soup s1 = a b b c and the rules r1 = a -> c c | (+, b), (-, [b b])
and r2 = b b -> b , r1 would replace the object 'a' with two copies of 'c', while r2 would halve the number of 'b' objects. However, there is a restriction, on r1: there must be a single 'b' in the soup, and not two, hence, in our situation, r2 must be applied first. Please note that [b b] =/= b b. the reason for this is that when you write (+, a b c d), if either one of the four objects is in the soup, the condition is met. So (+, a b c d) and (+, a a b b b c d) are would yield the same result. However, if one wants to test that multiple copies of an object exists, it is necessary to use square brackets e.g. (-, [a a a]) would ensure that there are at most two copies of 'a' in the soup.

Now that I have given you the background, let us focus on what I'm trying to do in Maude; consider the function :
op passesCond : Soup MRule -> Bool .
ceq passesCond(S1, S -> Smd | CS ) = 
        if (S3 [S4] := S2) /\ (-, S2) := INH 
        then (S1 & (S3 [S4]) == empty)
        else 
            (if (-, S2) := INH
            then (S1 & S2 == empty)
            fi)
        fi 
        if INH := CS .
where "&" is a function that performs the intersection of two Soups. 

At the moment, I encounter the following error: 
Maude> rewrites: 111319 in 270ms cpu (272ms real) (412292 rewrites/second)
Warning: Parse error in (passesCond(S1,P : S -> Smd | INH))=((if(S3[S4]:=
    <---*HERE*
Error: no parse for ceq passesCond(S1,P : S -> Smd | INH) ~ (if(S3[S4]:= S2)/\(
    -,S2):= NC then(S1 &(S3[S4])== empty)else(if(-,S2):= NC then(S1 & S2 ==
    empty)fi)fi)
Warning: Parse error in (passesCond(S1,P : S -> Smd | CS))=((if(S3[S4]:=
    <---*HERE*
Error: no parse for ceq passesCond(S1,P : S -> Smd | CS) ~ (if(S3[S4]:= S2)/\(
    -,S2):= NC then(S1 &(S3[S4])== empty)else(if(-,S2):= NC then(S1 & S2 ==
    empty)fi)fi)
Introduced module SEMANTICS

It seems to dislike the pattern S [S1] := S' as a valid pattern for a condition, and I've unsuccessfully tried for days to understand why. Can you help? Thank you in advance. 


Many thanks for your time and I look forward to your response.


Best wishes,
Mihai



-- 
Remember who you are, what you stand for and there will always be a way!