Maude-help mailing list

["Veselinov, Roman" <roma AT WPI.EDU>]

Hello,

 

My name is Roman and I am just starting to understand Maude with its syntax and semantics. I have couple of question (forgive me for not being specific enough) and I will be grateful if someone can guide me towards an answer:

 

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.

 

2. 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?

 

Thank you in advance for your help.

 

Regards,

 

Roman