Maude-help mailing list

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

Hi Roman,

On Thursday 27 September 2007 08:37, Veselinov, Roman wrote:
>  1.  I am designing a state transition system where the rules serve to
> transition from node to node with variable changing/rewritten within each
> node. The part I am trying to work out is that from each node there are
> transitions to more than one node - I have to explicitly write this using
> rules for each edge. Is there a way to have Maude choose from a pool of
> values for my variable instead of me explicitly doing that as in this ex:
>
> var A can be either 1,2 or 3.
>
> rl [1] : node(1) => node(2)
> rl [2] : node(1) => node(3)
> rl [3] : node(2) => node(1)
> rl [4] : node(2) => node(3)
> ....
> This is much more simple example and if there are more values for A and
> nodes the number of rl to be written grows exponentially. I understand
> node(1) => node(A) is illegal since the variable must be bounded so I am
> hoping for guidance on this.

I'm guessing your pool is a set and you don't allow self-loops.

mod AUTOMATA is
  inc SET{Nat} .

  sort State .
  op node : Nat -> State .
  
  vars N M : Nat .
  var Rest : Set{Nat} .

  crl node(N) => node(M) if (N, M, Rest) := (1, 2, 3) .
endm

search node(1) =>+ node(N) .

Note that the matching algorithm used to evaluate (N, M, Rest) := (1, 2, 3) 
is 
deterministic and thus not fair - which is irrelevant if you are going to 
explore all paths (search or model checker).

>  1.  The harder question for me is if Maude given two systems/modules can
> produce the synchronous product between them ( as in the product of two
> DFAs) and if yes how can this be done automatically?

Currently the only way of forcing the synchronization is to write your own 
interpreter at the metalevel that would pair one step searches from paired 
states - but then you have to keep your own state graph. In the future it 
will be possible to do this with the object level strategy language:

mod SYNC is
  inc AUTOMATA .

  sort ProductState .
  op _*_ : State State -> ProductState .

  vars S1 S2 S1' S2' : State .
  crl S1 * S2 => S1' * S2' if S1 => S1' /\ S2 => S2' [label sync] .
endm

*** all states reachable by 1 sync rewrite
srew node(1) * node(2) using sync{all,all} .

*** all states reachable by 1 or more sync rewrites
srew node(1) * node(2) using sync{all,all}+ .

but this only works in various alpha releases. Let me know if you want to be 
an alpha tester.

Steven