K-user mailing list

[Traian Florin Șerbănuță <traian.serbanuta AT info.uaic.ro>]

Hello,

The problem is that your rule

rule <k> system T:# Id ; _ process P:# Id (N:# Int) ;  endprocess ; _
endsystem ; => . ...</k>
(. =>  <process >
            <name> P </name>
           </process>)

matches and deletes the entire system when it creates the first process,

What you probably want is to process all process declarations sequentially.

One way to do that would be having a rule for going inside the system

rule system T:Id ;   C:Comp endsystem ; => C

(btw, using #Int, #Id, ... in K definition is now deprecated, with the strong suggestion you should use their semantical extensions Int, Id, ...)

Next, to sequentialize the declaration, you would need to replace your rule for the composition of process declarations to handle all declarations:

rule P1:Comp  P2:Comp  => P1 ~> P2

Finally, you will have to handle signal declarations as well, which you can erase for now with a rule like

rule signal _(); => .

Then your previous rule for creating a process will simply be:

rule <k>  process P:Id (N:Int) ;  endprocess ; => . ...</k>

(. =>  <process >

            <name> P </name>

           </process>)

Also, as you may want to sequentialize tasks within a process, too, it might be good to have the <k> cell be inside a process in the configuration, maybe naming the initial process which sets up a system with a specific name.

best wishes,

- traian

2013/3/12 samira kherfellah <samira.kherfellah AT gmail.com>

Hello,

I need your help, I want to redefine a language in K, this language is
composed of processes that communicate with signals.

The first goal is to display the list of processes.

-Here is an example program in this language:

system test ;

signal a();

process p(1) ;
//instructions
endprocess;

process q(1) ;
//instructions
endprocess;

endsystem;

-Syntax is given as follows:

module SYSTEM-SYNTAX
    syntax Sys ::= "system" Id ";"
                        Comp
                     "endsystem" ";"

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

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


    syntax Signaldecl ::= "signal" Id "(" ")" ";"

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

endmodule

module SYSTEM
  imports SYSTEM-SYNTAX

  configuration
<T>
  <k> $PGM:K </k>

  <process multiplicity="*" >
     <name> process </name>
  </process>

</T>


rule <k> system T:# Id ; _ process P:# Id (N:# Int) ;  endprocess ; _
endsystem ; => . ...</k>
(. =>  <process >
            <name> P </name>
           </process>)

rule P1:Processdecl  P2:Processdecl  => P1 ~> P2

endmodule

-I want to see the following execution:

<T>
  <k> .K </k>

  <process >
     <name> p </name>
  </process>

 <process >
     <name> q </name>
  </process>

</T>

-But I have this display:

<T>
  <k> .K </k>

  <process >
     <name> p </name>
  </process>

</T>

Waiting for your reply, please accept my respectful greetings.

Samira Kherfellah.
_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user