K-user mailing list

[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.