Maude-help mailing list

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

I haven't looked at the strategy language in almost 7 years; but culling from the various alpha release notes
here is the fragment that is currently supported by Core Maude:

srewrite [<nat>] in <module> : <term> using <strategy> .

Here the
  [<nat>]
(which specifies the number of solutions to find) and
  in <module> :
parts are optional. srewrite is a bit like search in that looks for
sequences of rewrites, but here the restriction on a sequence is that
it must satisfy the strategy.

Strategies are formed as follows; the leaf strategies are:

fail       produce the empty set of successors
idle       produce the identity rewrite
all        apply any rule
l          apply a rule with label l
l[s]       apply a rule with label l and substitution s

Substitions are a comma seperated list:
v1 <- t1 ,..., vk <- tk

The strategy combinators are:

s *        do s 0 or more times
s +        do s 1 or more times
s ; s'     do s and then s'
s | s'     do s or s'
t ? s : f  do t, if it produces results to s on them else do f on the
           original term

Note that at each step a strategy transforms a term into a set of
successors.

---

The modifier top(s) where s is an application strategy restricts
applications to the top of the current term.

The combinator s ! is similar to s * but only terms that cannot be
further rewritten by s are returned. It is implemented much more
efficiently than the equivalent _expression_ s * ; (s ? fail : idle)
because evaluation of the two occurences of s are combined.

The following unary branch combinators are implemented more
efficiently than the equivalent branch expressions:

           success        fail
=======================================================
not(s)           fail            idle
test(s)           idle            fail
try(s)           s            idle

Note that all other combinations in the result table are equivalent to
idle, fail, s or one of these 3 combinators.

---

Combinator:

  <strategy> or-else <strategy>

and the tests:

  match <pattern>
  match <pattern> s.t. <condition>
  xmatch <pattern>
  xmatch <pattern> s.t. <condition>
  amatch <pattern>
  amatch <pattern> s.t. <condition>

match = match at top
xmatch = match at top with extension for associative theories
amatch = match anywhere in term

---

The application of a label l in the strategy language can take a
list of  substrategies to use for rewrite condition fragments with the
syntax
  l{s, t}
or
  l[X <- u, Y <- v]{s, t}
if a substitution is included. It is now required that the number of
substrategies exactly match the number of rewrite condition fragments
in a rule for the rule to be considered for application (this might be
relaxed in the future).
The strategic searches for rewrite condition fragments are interleaved
with other branches of the original search, including branches from
the same crl application in order to achieve fairness.
Since the strategy combinators not() and test() can prune their search
after achieving a single success, it is possible start several
infinite searches and yet still terminate if one succeeds:

mod COUNT is
  inc NAT .
  sort Foo .
  op f : Nat -> Foo .
  op success : -> Foo .

var N : Nat .
  rl N => N + 2 [label 2] .

  crl f(N) => success if N => 9 [label a] .
  crl f(N) => success if N => 10 [label a] .
endm

*** check interleave of two infinite seaches, 1 successful, 1 not
srew f(0) using test(a{2 *}) .

Steven

On 6/11/13 9:01 AM, Morandi Benjamin wrote:

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

_______________________________________________
Maude-help mailing list
Maude-help AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/maude-help