package AvatarInstance { private import AvatarGeneral::*; private import AvatarBlockTypes::*; private import AvatarCommunication::*; private import AvatarTransitionServer::*; // DATATYPES $$$$$$$$$$$$$$$$$$$$$$$$ attribute def 'Point' :> '#AvatarDataType' { attribute x : Integer default := 0; attribute y : Integer default := 0; } // COMMUNICATIONS $$$$$$$$$$$$$$$$$$$$$$$$ // Relation Sync_Relation ============= part Sync_Relation: '#Sync_Rel' = '#Sync_Rel'('@block1' = blk0, '@block2' = blk1_0, '@private'=true); // Channel syn_in0_out1------------- part syn_in0_out1 : '#Sync' = '#Sync'('@relation' = Sync_Relation); binding : '#InSignalBinding' bind blk0.sig_in0 = syn_in0_out1; binding : '#OutSignalBinding' bind blk1_0.sig_out1 = syn_in0_out1; // Message of signal blk0.sig_in0............ part def msg_in0 :> '#InMessage' { private part '@channel' : '#Channel' = syn_in0_out1; attribute x : Integer; attribute p : 'Point'; attribute b : Boolean; } // Message of signal blk1_0.sig_out1............ part def msg_out1 :> '#OutMessage', msg_in0 { attribute x redefines x; attribute p redefines p; attribute b redefines b; } // Channel syn_out0_in1------------- part syn_out0_in1 : '#Sync' = '#Sync'('@relation' = Sync_Relation); binding : '#OutSignalBinding' bind blk0.sig_out0 = syn_out0_in1; binding : '#InSignalBinding' bind blk1_0.sig_in1 = syn_out0_in1; // Message of signal blk1_0.sig_in1............ part def msg_in1 :> '#InMessage' { private part '@channel' : '#Channel' = syn_out0_in1; attribute x : Integer; attribute p : 'Point'; attribute b : Boolean; } // Message of signal blk0.sig_out0............ part def msg_out0 :> '#OutMessage', msg_in1 { attribute x redefines x; attribute p redefines p; attribute b redefines b; } // BLOCKS $$$$$$$$$$$$$$$$$$$$$$$$ // Block blk1============= part blk1 : '#AvatarBlock' { // state-machine ------------------- exhibit state '@statemachine' : '#AvatarStateMachine' { entry action startstate :'#AvatarStartState'; transition : '#AvatarTransition' first startstate then stopstate; exit action stopstate :'#AvatarStopState'; } // Sub-Blocks øøøøøøøøøøøøøøøøøøøøøøø // Block blk1_0============= part blk1_0 : '#AvatarBlock' { // Attributes --------------------- attribute x : Integer := 0; attribute b : Boolean := false; attribute p : 'Point'; // Signals --------------------- part sig_in1 : '#Channel'; part sig_out1 : '#Channel'; // Timers --------------------- part tmr: '#AvatarTimer' = '#AvatarTimer'(); // state-machine ------------------- exhibit state '@statemachine' : '#AvatarStateMachine' { state send_out1_0 : '#AvatarSendState'; transition : '#AvatarTransition' first send_out1_0 then stopstate; state receive_in1_0 : '#AvatarReceiveState' = '#AvatarReceiveState'( '@request' = { '#SendRequest'( '@channel'= sig_out1, '@payload' = msg_out1( x, p, b ) ) } ); transition : '#AvatarTransition' first receive_in1_0 then send_out1_0; state state1 : '#AvatarStandardState' = '#AvatarStandardState'( '@pool' = {( '#AvatarSetTimerRequest'( '@channel'= tmr.'@set', '@payload' = '#TimerSetMsg'(10) ), '#ReceiveRequest'( '@index' = 2, '@channel'= sig_in1 ) )} ); transition : '#AvatarTransition' first state1 if '@index' == 1 then set_tmr_0; transition : '#AvatarTransition' first state1 if '@index' == 2 do action : '#ReceiveAction' { item '@msg' : msg_in1 = '@payload' as msg_in1; first start; then assign x := '@msg'.x; then assign p := '@msg'.p; then assign b := '@msg'.b; then done; } then receive_in1_0; state set_tmr_0 : '#AvatarSetTimerState'; transition : '#AvatarTransition' first set_tmr_0 then state2; state expire_tmr_0 : '#AvatarExpireTimerState'; transition : '#AvatarTransition' first expire_tmr_0 then state1; state state2 : '#AvatarStandardState' = '#AvatarStandardState'( '@pool' = {( '#AvatarExpireTimerRequest'( '@channel'= tmr.'@expire' ), '#AvatarResetTimerRequest'( '@index' = 2, '@channel'= tmr.'@reset', '@payload' = '#TimerResetMsg'() ) )} ); transition : '#AvatarTransition' first state2 if '@index' == 1 then expire_tmr_0; transition : '#AvatarTransition' first state2 if '@index' == 2 then reset_tmr_0; entry action startstate :'#AvatarStartState'; transition : '#AvatarTransition' first startstate then state1; state reset_tmr_0 : '#AvatarResetTimerState'; transition : '#AvatarTransition' first reset_tmr_0 then state2; exit action stopstate :'#AvatarStopState'; } } } // Block blk0============= part blk0 : '#AvatarBlock' { // Attributes --------------------- attribute x : Integer default := 0; attribute b : Boolean default := false; attribute p : 'Point'; attribute y : Integer default := 0; // Methods --------------------- calc make: '#AvatarCalcMethod' { attribute x : Integer; attribute y : Integer; return : 'Point'; } calc getx: '#AvatarCalcMethod' { attribute p : 'Point'; return : Integer; } action foo: '#AvatarVoidMethod' { attribute b : Boolean; attribute p : 'Point'; attribute x : Integer; } // Signals --------------------- part sig_in0 : '#Channel'; part sig_out0 : '#Channel'; // state-machine ------------------- exhibit state '@statemachine' : '#AvatarStateMachine' { state random_0 : '#AvatarRandomState' = '#AvatarRandomState'( '@request' = { if p.x > 4 ? '#immediate_request' else '#nok_request'(1) }, '@state_action' = '#Assignment'( '@target' = x, '@value' = '#bound_random'(0, p.y) ) ); transition : '#AvatarTransition' first random_0 do action : '#TransitionAction' { first start; then action = foo(b, p, x); then done; } then prercv_in0_0; state prercv_in0_0 : '#AvatarPreReceiveState' = '#AvatarPreReceiveState' ( '@request' = { '#ReceiveRequest'( '@channel'= sig_in0 ) } ); transition : '#AvatarTransition' first prercv_in0_0 do action : '#ReceiveAction' { item '@msg' : msg_in0 = '@payload' as msg_in0; first start; then assign x := '@msg'.x; then assign p := '@msg'.p; then assign b := '@msg'.b; then done; } then rcv_in0_0; exit action stopstate :'#AvatarStopState'; state snd_out0_0 : '#AvatarSendState'; transition : '#AvatarTransition' first snd_out0_0 do action : '#TransitionAction' { first start; then assign p:= make(x, y); then assign x:= getx(p); then done; } then random_0; entry action startstate :'#AvatarStartState' = '#AvatarStartState'( '@request' = { '#TrivialRequest'('@delay' = '#bound_random'(1, p.x)) } ); transition : '#AvatarTransition' first startstate do action : '#TransitionAction' { first start; then assign x:= 1; then assign b:= true; then assign p::x:= x; then done; } then presnd_out0_0; state presnd_out0_0 : '#AvatarPreSendState' = '#AvatarPreSendState' ( '@request' = { '#SendRequest'( '@channel'= sig_out0, '@payload' = msg_out0( x, p, b ) ) } ); transition : '#AvatarTransition' first presnd_out0_0 then snd_out0_0; state rcv_in0_0 : '#AvatarReceiveState'; transition : '#AvatarTransition' first rcv_in0_0 then stopstate; } } // Block Shortcut Links $$$$$$$$$$$$ part blk1_0 : '#AvatarBlock' :> blk1.blk1_0 = blk1.blk1_0; }