Synchronous Set Relations in Maude

Summary

Synchronous set relations provide a natural model for describing the operational semantics of synchronous languages. Intuitively, a synchronous rewrite relation selects redexes, according to some strategy, and reduces them in parallel. In the research community, it has been of interest the implementation of serialization procedures for simulating synchronous set relations by asynchronous term rewriting.

This prototype provides a minimalistic infrastructure in rewriting logic for simulating synchronous set relations that exploits the reflection capabilities of rewriting logic and its support for set rewriting, i.e., rewriting modulo axioms such as associativity, commutativity, and identity. The infrastructure consists of system module SMAUDE in Maude, defining a set of generic sorts and terms, the algebraic properties of the datatypes, and a set of functions and rewrite rules that support the synchronous execution of an atomic set relation. As a direct advantage of using this infrastructure, all commands in Maude for rewrite theories such as its rewrite and search commands, and formal verification tools such as Maude's LTL Model Checker, are directly available for analyzing formal properties of synchronous set relations.

Installation

The infrastructure is entirely written in Maude. The current version has been tested in Maude 2.6, but should work on earlier releases of Maude.

• Download the Maude source files

The main file in the infrastructure is smaude.maude.

Usage

You must first make sure the infrastructure is loaded. Assuming the main file in the source code smaude.maude is in the current directory and maude is your Maude executable, you can load it using the command:

[smaude] maude smaude.maude 

\||||||||||||||||||/

--- Welcome to Maude ---

/||||||||||||||||||\

Maude 2.6 built: Dec 10 2010 11:12:39

Copyright 1997-2010 SRI International

Mon Jun 13 10:46:55 2011

You use the infrastructure by extending system module SMAUDE, provided in smaude.maude, with concrete syntax for element names (sort Elm), attribute names (sort Aid), expressions (sort Expr), values (sort Val), and an evaluation eval for evaluating expressions. For a detailed explanation of these types and the predefined datatypes, please see the document at the bottom of the page.

Consider the following specification of a clock system in which hours and minutes are incremented synchronously:

mod CLOCKS is

 inc SMAUDE .

 --- Element ids for elements

 ops h m : Nat -> Eid [ctor] .

 --- Each element of a clock either displays hours in attribute 'hour'

 --- or  minutes in attribute 'min'.

 ops hour min : -> Aid [ctor] .

 --- Natural numbers are used as values

 subsort Nat < Val .

 ops hour min : Nat -> Expr [ctor] .

 --- Link the name of the module to the framework

 eq MODULE-NAME = 'CLOCKS .

 vars C N N' : Nat .

 var  CTX    : Ctx .

 var  M      : Map .

 --- Evaluation of min and hour attributes. The user defines equationally

 --- all expressions. The unary version of 'eval' can be used in the rules

 --- (see rule cl-2 for instance) and the framework will complete it with

 --- the current state

 eq eval(( < m(C) | min  : N, M > CTX) , min(C))  = N .

 eq eval(( < h(C) | hour : N, M > CTX) , hour(C)) = N .

 --- Reseting a clock (has the highest priority, indicated by the number 1 

 --- in its name)

 rl [cl-1] :

    < h(C) | hour : 11 > < m(C) | min : 59 >  

 => < h(C) | hour : 0 >  < m(C) | min : 0 > .

 --- Incrementing the hour of a clock

 rl [cl-2] :

    < h(C) | hour : N > 

 => if eval(min(C)) == 59

    then < h(C) | hour : s(N) >

    else < h(C) | hour : N >

    fi .

 --- Incrementing the minutes of a clock

 rl [cl-3] :

    < m(C) | min : N >

 => if N == 59

    then < m(C) | min : 0 > 

    else < m(C) | min : s(N) > 

    fi .

--- Initial state with two clocks showing 0:00

 op init : -> State .

 eq init = { < h(1) | hour : 0 > < m(1) | min : 0 >

             < h(2) | hour : 0 > < m(2) | min : 0 > } .

endm

In CLOCKS, hour elements use constructor h for element identifiers and have attribute hour as its single attribute. Minute elements use constructor m for element identifiers and have attribute min as its single attribute. Natural numbers are used as values for the attributes. The n-th clock is represented by the hour element with element identifier h(n) and the minute element with element identifier m(n). Attributes hour of an hour element h(n) (although never used in this example) and min of a minute element m(n) can be accessed by evaluating expressions hour(n) and min(n), respectively. A clock displaying 9:15, written in the syntax of CLOCKS, is

< h(1) | hour : 9 >  < min(1) | min : 15 >

Assuming file smaude.maude has been loaded, and file clocks.maude contains module CLOCKS, the following are regular Maude commands (interpreted synchronously) on state init:

Maude> load clocks.maude

Maude> rew [59] init .

rewrite [59] in CLOCKS-PREDS : init .

rewrites: 20351 in 1602ms cpu (1605ms real) (12698 rewrites/second)

result SState: {< h(1) | hour : 0 > < h(2) | hour : 0 > < m(1) | min : 59 > < m(2) | min : 59 >}

Maude> rew [60] init .

rewrite [60] in CLOCKS-PREDS : init .

rewrites: 20461 in 1599ms cpu (1609ms real) (12794 rewrites/second)

result SState: {< h(1) | hour : 1 > < h(2) | hour : 1 > < m(1) | min : 0 > < m(2) | min : 0 >}

Maude> search init =>1 X:State .

search in CLOCKS-PREDS : init =>1 x:State .

Solution 1 (state 1)

states: 2  rewrites: 342 in 28ms cpu (28ms real) (11992 rewrites/second)

x:State --> {< h(1) | hour : 0 > < h(2) | hour : 0 > < m(1) | min : 1 > < m(2) | min : 1 >}

For an extended version of this example, including the verification of some LTL properties of CLOCKS, please see the examples included with the current distributions.

Publications

The infrastructure is described in the following paper: