Maude-help mailing list

["Morandi Benjamin" <benjamin.morandi AT inf.ethz.ch>]

Hi Steven,

 

I am using the following transition rule for parallelism in a structural operational semantics for concurrency [1]. The concurrent processors are separated by the associative and commutative | operator, and σ is the program state. Using the associativity and commutatively of |, this rule looks for any processor that can make progress using one of the other transition rules, e.g., the following rule for locking a set of processors ‘qs’:

 

op _ | _ : ActionQueueList ActionQueueList -> ActionQueueList [ctor assoc comm prec 122 format (d d ni d)]

crl [parallelism] : Γ |- aqs1 | aqs' , σx => Γ |- aqs2 | aqs, σy

                if

                                Γ |- aqs1, σx => Γ |- aqs2 , σy /\

                                not (aqs1 == aqs2 and σx == σy) . *** Prevent infinite application of this rule by making sure something changes in the system

 

crl [lock] : Γ |- p :: lock(qs) ; sp, σ => Γ |- p :: sp, σ'

                if

                                σ . isUnlocked(qs) /\

                                σ' := σ .lock(p, qs) .

 

<more rules>

 

How could I specify in the ‘srew’ command that it should use the parallelism rule, which itself should use the lock rule to satisfy its condition? I am looking for ways to steer the rewrite process in a concurrent system. Thank you very much for your help.

 

Best regards

 

Benjamin

 

[1] Full semantics, https://bitbucket.org/bmorandi/scoop-executable-formal-specification/src

 

 

 

From: maude-help-bounces AT cs.uiuc.edu [mailto:maude-help-bounces AT cs.uiuc.edu] On Behalf Of Steven Eker
Sent: Thursday, May 30, 2013 10:26 PM
To: maude-help AT cs.uiuc.edu
Subject: Re: [Maude-help] Rewrite, change, and continue

 

For small values of n you could label the rules and use the built-in fragment of the Maude strategy language:

mod TEST is
  pr NAT .
  ops f g : Nat -> Nat .
  op h : Nat Nat -> Nat .

var N : Nat .
  crl f(N) => g(N + 1) if N < 20 [label s] .
  crl g(N) => f(N + 1) if N rem 5 =/= 0 [label s] .

  rl f(N) => h(N, g(N)) [label m] .
endm

srew f(0) using s ; s ; s ; s ; m ; s ! .

This returns terms that result from 4 applications of an s rule, one application of an m rule, and then applications of s rules until no more s rules apply.

Steven

On 5/22/13 4:46 AM, Morandi Benjamin wrote:

Dear All,

 

I would like to achieve the following:

 

-          Rewrite a starting term ‘t’ ‘n’-times using ‘rew[n]’ and a set of rules ‘s’. The resulting term is ‘tt’.

-          Change ‘tt’ by manually applying a rule that is not in ‘s’. The resulting term is ‘ttt’.

-          Continue rewriting ‘ttt’ using ‘cont .’ and  the rules in ‘s’.

 

More generally, I’d like to influence which rule the rewrite command picks at a breakpoint of my choosing. Does anyone have an idea on how to do that?

 

Best regards

 

Benjamin Morandi

_______________________________________________

Maude-help mailing list

Maude-help AT cs.uiuc.edu

http://lists.cs.uiuc.edu/mailman/listinfo/maude-help

 

---

No virus found in this message.
Checked by AVG - www.avg.com
Version: 2013.0.3343 / Virus Database: 3184/6370 - Release Date: 05/30/13