k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

[K-user] Communication of processes

From: samira kherfellah <samira.kherfellah AT gmail.com>
To: k-user AT cs.uiuc.edu
Subject: [K-user] Communication of processes
Date: Thu, 14 Mar 2013 10:12:29 +0100
List-archive: <http://lists.cs.uiuc.edu/pipermail/k-user/>
List-id: <k-user.cs.uiuc.edu>

Hello,

In my system, processes communicate with messages and each process has
its own message queue that is initially empty

-if a process executes the transition:
output s() to {q} 0;
Then he adds a message "s" in the message queue of the process q

-if a process executes the transition:
input s().
then it removes a message "s" from its message queue.

-I want to represent it in K.

-I have an example of a test program:
system s;
signal s();

process p(1);
state init ;
output s() to {q}0;
nextstate init;
endstate;
endprocess;

process q(1);
state init;
input s();
nextstate init;
endstate;
endprocess;

endsystem;

-Language syntax is:

module IF-SYNTAX
imports BUILTIN-SYNTAX-HOOKS

syntax Sys ::= "system" Id ";"
Comp
"endsystem" ";"

syntax Id ::= "system" | "process" | "signal"

syntax Comp ::= Signaldecl| Processdecl
|Comp Comp [left]

syntax Signaldecl ::= "signal" Id SuiteS ";"

syntax SuiteS ::= "(" Exp ")"
|"(" ")"

syntax Processdecl ::= "process" Id "(" Int ")" ";"
ProcessComp
"endprocess" ";"

syntax ProcessComp ::= State
|ProcessComp ProcessComp [left]

syntax State ::= "state" Id ";"
StateComp
"endstate" ";"

syntax StateComp ::= Transition
|State

syntax Transition ::= Input Statement Terminator
|Statement Terminator

syntax Input ::= "input" Id "(" ")" ";"
| Input Input [left]

syntax Statement ::= Action
//| if then else
//| while do
| Statement Statement [left]

syntax Action ::= "skip" ";"
| "task" Exp ";"
| "output" Id Suite ";" //signal output

syntax Suite ::= "(" ")"
| "(" ")" "to" "{" Id "}" Int

syntax Terminator ::= "stop" ";"
|"nextstate" Id ";"

endmodule

-Configuration is:

configuration
<T color="yellow">

<instances color="Fuchsia">

<process multiplicity="*" color="red">
<k color="green"> $PGM:K </k>

<pid color="yellow"> process </pid>

<queue color="red"> .List </queue>

<msgs color="green">
<signale multiplicity="*" color="red">
<from> process</from>
<to color="red" > process </to>
<body color="yellow"> .K </body>
</signale>
</msgs>
</process>
</instances>

</T>

-OUTPUT rule is:

rule <pid> P </pid> <k> ouput S() to {Q} 0 ; => . ...</k>
(. => <process>
<pid > Q </pid>

<queue> ListItem(S) </queue>
</process>)

-But when I execute, it does not display the list of msgs?

Thank you for your help.

Samira

[K-user] Communication of processes, samira kherfellah, 03/14/2013
- Re: [K-user] Communication of processes, Traian Florin Șerbănuță, 03/15/2013