Skip to content
Snippets Groups Projects
Commit bd6ed3ed authored by Sophie Coudert's avatar Sophie Coudert
Browse files

complete one test for error cases (done)

parent 727f4c5e
No related branches found
No related tags found
2 merge requests!508Avatar sys ml 04 2024,!507Avatar sys ml 04 2024
package AvatarInstance {
private import AvatarGeneral::*;
private import AvatarBlockTypes::*;
private import AvatarCommunication::*;
private import AvatarTransitionServer::*;
// DATATYPES $$$$$$$$$$$$$$$$$$$$$$$$
attribute def '@dt:Point' :> '#AvatarDataType' {
attribute 'x' : Integer default := 0;
attribute 'y' : Integer default := 0;
}
// COMMUNICATIONS $$$$$$$$$$$$$$$$$$$$$$$$
// Relation '@SYN0:B0-B1'=============
part '@SYN0:B0-B1': '#Sync_Rel' = '#Sync_Rel'('@block1' = '@blk:B0', '@block2' = '@blk:B1', '@private'=true);
// Channel '@syn:B0.in0<B1.out1'-------------
part '@syn:B0.in0<B1.out1' : '#Sync' = '#Sync'('@relation' = '@SYN0:B0-B1');
binding : '#InSignalBinding' bind '@blk:B0'.'@sig:in0' = '@syn:B0.in0<B1.out1';
binding : '#OutSignalBinding' bind '@blk:B1'.'@sig:out1' = '@syn:B0.in0<B1.out1';
// Message of signal '@blk:B0'.'@sig:in0'............
part def '@MSG:B0.in0' :> '#InMessage' {
private part '@channel' : '#Channel' = '@syn:B0.in0<B1.out1';
attribute 'x' : Integer;
attribute 'p' : '@dt:Point';
attribute 'b' : Boolean;
}
// Message of signal '@blk:B1'.'@sig:out1'............
part def '@MSG:B1.out1' :> '#OutMessage', '@MSG:B0.in0' {
attribute 'x' redefines 'a';
attribute 'p' redefines 'p';
attribute 'b' redefines 'b';
}
// Channel '@syn:B0.out0>B1.in1'-------------
part '@syn:B0.out0>B1.in1' : '#Sync' = '#Sync'('@relation' = '@SYN0:B0-B1');
binding : '#OutSignalBinding' bind '@blk:B0'.'@sig:out0' = '@syn:B0.out0>B1.in1';
binding : '#InSignalBinding' bind '@blk:B1'.'@sig:in1' = '@syn:B0.out0>B1.in1';
// Message of signal '@blk:B1'.'@sig:in1'............
part def '@MSG:B1.in1' :> '#InMessage' {
private part '@channel' : '#Channel' = '@syn:B0.out0>B1.in1';
attribute 'x' : Integer;
attribute 'p' : '@dt:Point';
attribute 'b' : Boolean;
}
// Message of signal '@blk:B0'.'@sig:out0'............
part def '@MSG:B0.out0' :> '#OutMessage', '@MSG:B1.in1' {
attribute 'x' redefines 'x';
attribute 'p' redefines 'p';
attribute 'b' redefines 'b';
}
// BLOCKS $$$$$$$$$$$$$$$$$$$$$$$$
// Block '@blk:B0'=============
part '@blk:B0' : '#AvatarBlock' {
// Attributes ---------------------
attribute '$x' : Integer default := 0;
attribute '$b' : Boolean default := false;
attribute '$p' : '@dt:Point';
attribute '$y' : Integer default := 0;
// Methods ---------------------
calc '$make': '#AvatarCalcMethod' {
attribute 'x' : Integer;
attribute 'y' : Integer;
return : '@dt:Point';
}
calc '$getx': '#AvatarCalcMethod' {
attribute 'p' : '@dt:Point';
return : Integer;
}
action '$foo': '#AvatarVoidMethod' {
attribute 'x' : Integer;
attribute 'p' : '@dt:Point';
attribute 'b' : Boolean;
}
// Signals ---------------------
part '@sig:in0' : '#Channel';
part '@sig:out0' : '#Channel';
// state-machine -------------------
exhibit state '@statemachine' : '#AvatarStateMachine' {
exit action '@st:stop' :'#AvatarStopState';
state '@st:receive.in0.0' : '#AvatarReceiveState';
transition : '#AvatarTransition' first '@st:receive.in0.0'
then '@st:stop';
state '@st:send.out0.0' : '#AvatarSendState';
transition : '#AvatarTransition' first '@st:send.out0.0'
do action : '#TransitionAction' {
first start;
then assign '$p':= '$make'('$x', '$y');
then assign '$x':= '$getx'('$p');
then done;
} then '@st:random.0';
entry action '@st:start' :'#AvatarStartState' = '#AvatarStartState'(
'@request' = {
'#TrivialRequest'('@delay' = '#bound_random'(1, '$p'.'x'))
}
);
transition : '#AvatarTransition' first '@st:start'
do action : '#TransitionAction' {
first start;
then assign '$x':= 1;
then assign '$b':= true;
then assign '$p'::'x':= '$x';
then done;
} then '@st:presend.out0.0';
state '@st:presend.out0.0' : '#AvatarPreSendState' = '#AvatarPreSendState' (
'@request' = {
'#SendRequest'(
'@channel'= '@sig:out0',
'@payload' = '@MSG:B0.out0'(
'$x',
'$p',
'$b' )
)
}
);
transition : '#AvatarTransition' first '@st:presend.out0.0' then '@st:send.out0.0';
state '@st: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 '@st:random.0'
do action : '#TransitionAction' {
first start;
then action = '$foo'('$x', '$p', '$b');
then done;
} then '@st:prereceive.in0.0';
state '@st:prereceive.in0.0' : '#AvatarPreReceiveState' = '#AvatarPreReceiveState' (
'@request' = {
'#ReceiveRequest'(
'@channel'= '@sig:in0'
)
}
);
transition : '#AvatarTransition' first '@st:prereceive.in0.0'
do action : '#ReceiveAction' {
item '@msg' : '@MSG:B0.in0' = '@payload' as '@MSG:B0.in0';
first start;
then assign '$x' := '@msg'.'x';
then assign '$p' := '@msg'.'p';
then assign '$b' := '@msg'.'b';
then done;
} then '@st:receive.in0.0';
}
}
// Block '@blk:B1'=============
part '@blk:B1' : '#AvatarBlock' {
// Attributes ---------------------
attribute '$x' : Integer := 0;
attribute '$b' : Boolean := false;
attribute '$p' : '@dt:Point';
// Signals ---------------------
part '@sig:in1' : '#Channel';
part '@sig:out1' : '#Channel';
// state-machine -------------------
exhibit state '@statemachine' : '#AvatarStateMachine' {
state '@st:receive.in1.0' : '#AvatarReceiveState' = '#AvatarReceiveState'(
'@request' = {
'#SendRequest'(
'@channel'= '@sig:out1',
'@payload' = '@MSG:B1.out1'(
'$x',
'$p',
'$b' )
)
}
);
transition : '#AvatarTransition' first '@st:receive.in1.0'
then '@st:send.out1.0';
state '@st:send.out1.0' : '#AvatarSendState';
transition : '#AvatarTransition' first '@st:send.out1.0'
then '@st:stop';
exit action '@st:stop' :'#AvatarStopState';
entry action '@st:start' :'#AvatarStartState' = '#AvatarStartState'(
'@request' = {
'#ReceiveRequest'(
'@channel'= '@sig:in1'
)
}
);
transition : '#AvatarTransition' first '@st:start'
do action : '#ReceiveAction' {
item '@msg' : '@MSG:B1.in1' = '@payload' as '@MSG:B1.in1';
first start;
then assign '$x' := '@msg'.'x';
then assign '$p' := '@msg'.'p';
then assign '$b' := '@msg'.'b';
then done;
} then '@st:receive.in1.0';
}
}
// Block Shortcut Links $$$$$$$$$$$$
}
package AvatarInstance {
private import AvatarGeneral::*;
private import AvatarBlockTypes::*;
private import AvatarCommunication::*;
private import AvatarTransitionServer::*;
// DATATYPES $$$$$$$$$$$$$$$$$$$$$$$$
attribute def '@dt:Point' :> '#AvatarDataType' {
attribute 'x' : Integer default := 0;
attribute 'y' : Integer default := 0;
}
// COMMUNICATIONS $$$$$$$$$$$$$$$$$$$$$$$$
// Relation '@SYN0:B0-B1'=============
part '@SYN0:B0-B1': '#Sync_Rel' = '#Sync_Rel'('@block1' = '@blk:B0', '@block2' = '@blk:B1', '@private'=true);
// Channel '@syn:B0.in0<B1.out1'-------------
part '@syn:B0.in0<B1.out1' : '#Sync' = '#Sync'('@relation' = '@SYN0:B0-B1');
binding : '#InSignalBinding' bind '@blk:B0'.'@sig:in0' = '@syn:B0.in0<B1.out1';
binding : '#OutSignalBinding' bind '@blk:B1'.'@sig:out1' = '@syn:B0.in0<B1.out1';
// Message of signal '@blk:B0'.'@sig:in0'............
part def '@MSG:B0.in0' :> '#InMessage' {
private part '@channel' : '#Channel' = '@syn:B0.in0<B1.out1';
attribute 'x' : Integer;
attribute 'p' : '@dt:Point';
attribute 'b' : Boolean;
}
// Message of signal '@blk:B1'.'@sig:out1'............
part def '@MSG:B1.out1' :> '#OutMessage', '@MSG:B0.in0' {
attribute 'x' redefines 'x';
attribute 'p' redefines 'p';
attribute 'b' redefines 'b';
}
// Channel '@syn:B0.out0>B1.in1'-------------
part '@syn:B0.out0>B1.in1' : '#Sync' = '#Sync'('@relation' = '@SYN0:B0-B1');
binding : '#OutSignalBinding' bind '@blk:B0'.'@sig:out0' = '@syn:B0.out0>B1.in1';
binding : '#InSignalBinding' bind '@blk:B1'.'@sig:in1' = '@syn:B0.out0>B1.in1';
// Message of signal '@blk:B1'.'@sig:in1'............
part def '@MSG:B1.in1' :> '#InMessage' {
private part '@channel' : '#Channel' = '@syn:B0.out0>B1.in1';
attribute 'x' : Integer;
attribute 'p' : '@dt:Point';
attribute 'b' : Boolean;
}
// Message of signal '@blk:B0'.'@sig:out0'............
part def '@MSG:B0.out0' :> '#OutMessage', '@MSG:B1.in1' {
attribute 'x' redefines 'x';
attribute 'p' redefines 'p';
attribute 'b' redefines 'b';
}
// BLOCKS $$$$$$$$$$$$$$$$$$$$$$$$
// Block '@blk:B0'=============
part '@blk:B0' : '#AvatarBlock' {
// Attributes ---------------------
attribute '$x' : Integer default := 0;
// attribute '$b' : Boolean default := false;
attribute '$p' : '@dt:Point';
attribute '$y' : Integer default := 0;
// Methods ---------------------
calc '$make': '#AvatarCalcMethod' {
attribute 'x' : Integer;
attribute 'y' : Integer;
return : '@dt:Point';
}
calc '$getx': '#AvatarCalcMethod' {
attribute 'p' : '@dt:Point';
return : Integer;
}
action '$foo': '#AvatarVoidMethod' {
attribute 'x' : Integer;
attribute 'p' : '@dt:Point';
attribute 'b' : Boolean;
}
// Signals ---------------------
part '@sig:in0' : '#Channel';
part '@sig:out0' : '#Channel';
// state-machine -------------------
exhibit state '@statemachine' : '#AvatarStateMachine' {
exit action '@st:stop' :'#AvatarStopState';
state '@st:receive.in0.0' : '#AvatarReceiveState';
transition : '#AvatarTransition' first '@st:receive.in0.0'
then '@st:stop';
state '@st:send.out0.0' : '#AvatarSendState';
transition : '#AvatarTransition' first '@st:send.out0.0'
do action : '#TransitionAction' {
first start;
then assign '$p':= '$make'('$x', '$y');
then assign '$x':= '$getx'('$p');
then done;
} then '@st:random.0';
entry action '@st:start' :'#AvatarStartState' = '#AvatarStartState'(
'@request' = {
'#TrivialRequest'('@delay' = '#bound_random'(1, '$p'.'x'))
}
);
transition : '#AvatarTransition' first '@st:start'
do action : '#TransitionAction' {
first start;
then assign '$x':= 1;
then assign '$b':= true;
then assign '$p'::'x':= '$x';
then done;
} then '@st:presend.out0.0';
state '@st:presend.out0.0' : '#AvatarPreSendState' = '#AvatarPreSendState' (
'@request' = {
'#SendRequest'(
'@channel'= '@sig:out0',
'@payload' = '@MSG:B0.out0'(
'$x',
'$p',
'$b' )
)
}
);
transition : '#AvatarTransition' first '@st:presend.out0.0' then '@st:send.out0.0';
state '@st: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 '@st:random.0'
do action : '#TransitionAction' {
first start;
then action = '$foo'('$x', '$p', '$b');
then done;
} then '@st:prereceive.in0.0';
state '@st:prereceive.in0.0' : '#AvatarPreReceiveState' = '#AvatarPreReceiveState' (
'@request' = {
'#ReceiveRequest'(
'@channel'= '@sig:in0'
)
}
);
transition : '#AvatarTransition' first '@st:prereceive.in0.0'
do action : '#ReceiveAction' {
item '@msg' : '@MSG:B0.in0' = '@payload' as '@MSG:B0.in0';
first start;
then assign '$x' := '@msg'.'x';
then assign '$p' := '@msg'.'p';
then assign '$b' := '@msg'.'b';
then done;
} then '@st:receive.in0.0';
}
}
// Block '@blk:B1'=============
part '@blk:B1' : '#AvatarBlock' {
// Attributes ---------------------
attribute '$x' : Integer := 0;
attribute '$b' : Boolean := false;
attribute '$p' : '@dt:Point';
// Signals ---------------------
part '@sig:in1' : '#Channel';
part '@sig:out1' : '#Channel';
// state-machine -------------------
exhibit state '@statemachine' : '#AvatarStateMachine' {
state '@st:receive.in1.0' : '#AvatarReceiveState' = '#AvatarReceiveState'(
'@request' = {
'#SendRequest'(
'@channel'= '@sig:out1',
'@payload' = '@MSG:B1.out1'(
'$x',
'$p',
'$b' )
)
}
);
transition : '#AvatarTransition' first '@st:receive.in1.0'
then '@st:send.out1.0';
state '@st:send.out1.0' : '#AvatarSendState';
transition : '#AvatarTransition' first '@st:send.out1.0'
then '@st:stop';
exit action '@st:stop' :'#AvatarStopState';
entry action '@st:start' :'#AvatarStartState' = '#AvatarStartState'(
'@request' = {
'#ReceiveRequest'(
'@channel'= '@sig:in1'
)
}
);
transition : '#AvatarTransition' first '@st:start'
do action : '#ReceiveAction' {
item '@msg' : '@MSG:B1.in1' = '@payload' as '@MSG:B1.in1';
first start;
then assign '$x' := '@msg'.'x';
then assign '$p' := '@msg'.'p';
then assign '$b' := '@msg'.'b';
then done;
} then '@st:receive.in1.0';
}
}
// Block Shortcut Links $$$$$$$$$$$$
}
package AvatarInstance {
private import AvatarGeneral::*;
private import AvatarBlockTypes::*;
private import AvatarCommunication::*;
private import AvatarTransitionServer::*;
// DATATYPES $$$$$$$$$$$$$$$$$$$$$$$$
attribute def '@dt:Point' :> '#AvatarDataType' {
attribute 'x' : Integer default := 0;
attribute 'y' : Integer default := 0;
}
// COMMUNICATIONS $$$$$$$$$$$$$$$$$$$$$$$$
// Relation '@SYN0:B0-B1'=============
part '@SYN0:B0-B1': '#Sync_Rel' = '#Sync_Rel'('@block1' = '@blk:B0', '@private'=true);
// Channel '@syn:B0.in0<B1.out1'-------------
part '@syn:B0.in0<B1.out1' : '#Sync' = '#Sync'('@relation' = '@SYN0:B0-B1');
binding : '#InSignalBinding' bind '@blk:B0'.'@sig:in0' = '@syn:B0.in0<B1.out1';
binding : '#OutSignalBinding' bind '@blk:B1'.'@sig:out1' = '@syn:B0.in0<B1.out1';
// Message of signal '@blk:B0'.'@sig:in0'............
part def '@MSG:B0.in0' :> '#InMessage' {
private part '@channel' : '#Channel' = '@syn:B0.in0<B1.out1';
attribute 'x' : Integer;
attribute 'p' : '@dt:Point';
attribute 'b' : Boolean;
}
// Message of signal '@blk:B1'.'@sig:out1'............
part def '@MSG:B1.out1' :> '#OutMessage', '@MSG:B0.in0' {
attribute 'x' redefines 'x';
attribute 'p' redefines 'p';
attribute 'b' redefines 'b';
}
// Channel '@syn:B0.out0>B1.in1'-------------
part '@syn:B0.out0>B1.in1' : '#Sync' = '#Sync'('@relation' = '@SYN0:B0-B1');
binding : '#OutSignalBinding' bind '@blk:B0'.'@sig:out0' = '@syn:B0.out0>B1.in1';
binding : '#InSignalBinding' bind '@blk:B1'.'@sig:in1' = '@syn:B0.out0>B1.in1';
// Message of signal '@blk:B1'.'@sig:in1'............
part def '@MSG:B1.in1' :> '#InMessage' {
private part '@channel' : '#Channel' = '@syn:B0.out0>B1.in1';
attribute 'x' : Integer;
attribute 'p' : '@dt:Point';
attribute 'b' : Boolean;
}
// Message of signal '@blk:B0'.'@sig:out0'............
part def '@MSG:B0.out0' :> '#OutMessage', '@MSG:B1.in1' {
attribute 'x' redefines 'x';
attribute 'p' redefines 'p';
attribute 'b' redefines 'b';
}
// BLOCKS $$$$$$$$$$$$$$$$$$$$$$$$
// Block '@blk:B0'=============
part '@blk:B0' : '#AvatarBlock' {
// Attributes ---------------------
attribute '$x' : Integer default := 0;
attribute '$b' : Boolean default := false;
attribute '$p' : '@dt:Point';
attribute '$y' : Integer default := 0;
// Methods ---------------------
calc '$make': '#AvatarCalcMethod' {
attribute 'x' : Integer;
attribute 'y' : Integer;
return : '@dt:Point';
}
calc '$getx': '#AvatarCalcMethod' {
attribute 'p' : '@dt:Point';
return : Integer;
}
action '$foo': '#AvatarVoidMethod' {
attribute 'x' : Integer;
attribute 'p' : '@dt:Point';
attribute 'b' : Boolean;
}
// Signals ---------------------
part '@sig:in0' : '#Channel';
part '@sig:out0' : '#Channel';
// state-machine -------------------
exhibit state '@statemachine' : '#AvatarStateMachine' {
exit action '@st:stop' :'#AvatarStopState';
state '@st:receive.in0.0' : '#AvatarReceiveState';
transition : '#AvatarTransition' first '@st:receive.in0.0'
then '@st:stop';
state '@st:send.out0.0' : '#AvatarSendState';
transition : '#AvatarTransition' first '@st:send.out0.0'
do action : '#TransitionAction' {
first start;
then assign '$p':= '$make'('$x', '$y');
then assign '$x':= '$getx'('$p');
then done;
} then '@st:random.0';
entry action '@st:start' :'#AvatarStartState' = '#AvatarStartState'(
'@request' = {
'#TrivialRequest'('@delay' = '#bound_random'(1, '$p'.'x'))
}
);
transition : '#AvatarTransition' first '@st:start'
do action : '#TransitionAction' {
first start;
then assign '$x':= 1;
then assign '$b':= true;
then assign '$p'::'x':= '$x';
then done;
} then '@st:presend.out0.0';
state '@st:presend.out0.0' : '#AvatarPreSendState' = '#AvatarPreSendState' (
'@request' = {
'#SendRequest'(
'@channel'= '@sig:out0',
'@payload' = '@MSG:B0.out0'(
'$x',
'$p',
'$b' )
)
}
);
transition : '#AvatarTransition' first '@st:presend.out0.0' then '@st:send.out0.0';
state '@st: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 '@st:random.0'
do action : '#TransitionAction' {
first start;
then action = '$foo'('$x', '$p', '$b');
then done;
} then '@st:prereceive.in0.0';
state '@st:prereceive.in0.0' : '#AvatarPreReceiveState' = '#AvatarPreReceiveState' (
'@request' = {
'#ReceiveRequest'(
'@channel'= '@sig:in0'
)
}
);
transition : '#AvatarTransition' first '@st:prereceive.in0.0'
do action : '#ReceiveAction' {
item '@msg' : '@MSG:B0.in0' = '@payload' as '@MSG:B0.in0';
first start;
then assign '$x' := '@msg'.'x';
then assign '$p' := '@msg'.'p';
then assign '$b' := '@msg'.'b';
then done;
} then '@st:receive.in0.0';
}
}
// Block '@blk:B1'=============
part '@blk:B1' : '#AvatarBlock' {
// Attributes ---------------------
attribute '$x' : Integer := 0;
attribute '$b' : Boolean := false;
attribute '$p' : '@dt:Point';
// Signals ---------------------
part '@sig:in1' : '#Channel';
part '@sig:out1' : '#Channel';
// state-machine -------------------
exhibit state '@statemachine' : '#AvatarStateMachine' {
state '@st:receive.in1.0' : '#AvatarReceiveState' = '#AvatarReceiveState'(
'@request' = {
'#SendRequest'(
'@channel'= '@sig:out1',
'@payload' = '@MSG:B1.out1'(
'$x',
'$p',
'$b' )
)
}
);
transition : '#AvatarTransition' first '@st:receive.in1.0'
then '@st:send.out1.0';
state '@st:send.out1.0' : '#AvatarSendState';
transition : '#AvatarTransition' first '@st:send.out1.0'
then '@st:stop';
exit action '@st:stop' :'#AvatarStopState';
entry action '@st:start' :'#AvatarStartState' = '#AvatarStartState'(
'@request' = {
'#ReceiveRequest'(
'@channel'= '@sig:in1'
)
}
);
transition : '#AvatarTransition' first '@st:start'
do action : '#ReceiveAction' {
item '@msg' : '@MSG:B1.in1' = '@payload' as '@MSG:B1.in1';
first start;
then assign '$x' := '@msg'.'x';
then assign '$p' := '@msg'.'p';
then assign '$b' := '@msg'.'b';
then done;
} then '@st:receive.in1.0';
}
}
// Block Shortcut Links $$$$$$$$$$$$
}
package AvatarInstance {
private import AvatarGeneral::*;
private import AvatarBlockTypes::*;
private import AvatarCommunication::*;
private import AvatarTransitionServer::*;
// DATATYPES $$$$$$$$$$$$$$$$$$$$$$$$
attribute def '@dt:Point' :> '#AvatarDataType' {
attribute 'x' : Integer default := 0;
attribute 'y' : Integer default := 0;
}
// COMMUNICATIONS $$$$$$$$$$$$$$$$$$$$$$$$
// Relation '@SYN0:B0-B1'=============
part '@SYN0:B0-B1': '#Sync_Rel' = '#Sync_Rel'('@block1' = '@blk:B0', '@block2' = '@blk:B1', '@private'=true);
// Channel '@syn:B0.in0<B1.out1'-------------
part '@syn:B0.in0<B1.out1' : '#Sync' = '#Sync'('@relation' = '@SYN0:B0-B1');
binding : '#InSignalBinding' bind '@blk:B0'.'@sig:in0' = '@syn:B0.in0<B1.out1';
binding : '#OutSignalBinding' bind '@blk:B1'.'@sig:out1' = '@syn:B0.in0<B1.out1';
// Message of signal '@blk:B0'.'@sig:in0'............
part def '@MSG:B0.in0' :> '#InMessage' {
private part '@channel' : '#Channel' = '@syn:B0.in0<B1.out1';
attribute 'x' : Integer;
attribute 'p' : '@dt:Point';
attribute 'b' : Boolean;
}
// Message of signal '@blk:B1'.'@sig:out1'............
part def '@MSG:B1.out1' :> '#OutMessage', '@MSG:B0.in0' {
attribute 'x' redefines 'x';
attribute 'p' redefines 'p';
attribute 'b' redefines 'b';
}
// Channel '@syn:B0.out0>B1.in1'-------------
part '@syn:B0.out0>B1.in1' : '#Sync' = '#Sync'('@relation' = '@SYN0:B0-B1');
// binding : '#OutSignalBinding' bind '@blk:B0'.'@sig:out0' = '@syn:B0.out0>B1.in1';
binding : '#InSignalBinding' bind '@blk:B1'.'@sig:in1' = '@syn:B0.out0>B1.in1';
// Message of signal '@blk:B1'.'@sig:in1'............
part def '@MSG:B1.in1' :> '#InMessage' {
private part '@channel' : '#Channel' = '@syn:B0.out0>B1.in1';
attribute 'x' : Integer;
attribute 'p' : '@dt:Point';
attribute 'b' : Boolean;
}
// Message of signal '@blk:B0'.'@sig:out0'............
part def '@MSG:B0.out0' :> '#OutMessage', '@MSG:B1.in1' {
attribute 'x' redefines 'x';
attribute 'p' redefines 'p';
attribute 'b' redefines 'b';
}
// BLOCKS $$$$$$$$$$$$$$$$$$$$$$$$
// Block '@blk:B0'=============
part '@blk:B0' : '#AvatarBlock' {
// Attributes ---------------------
attribute '$x' : Integer default := 0;
attribute '$b' : Boolean default := false;
attribute '$p' : '@dt:Point';
attribute '$y' : Integer default := 0;
// Methods ---------------------
calc '$make': '#AvatarCalcMethod' {
attribute 'x' : Integer;
attribute 'y' : Integer;
return : '@dt:Point';
}
calc '$getx': '#AvatarCalcMethod' {
attribute 'p' : '@dt:Point';
return : Integer;
}
action '$foo': '#AvatarVoidMethod' {
attribute 'x' : Integer;
attribute 'p' : '@dt:Point';
attribute 'b' : Boolean;
}
// Signals ---------------------
part '@sig:in0' : '#Channel';
part '@sig:out0' : '#Channel';
// state-machine -------------------
exhibit state '@statemachine' : '#AvatarStateMachine' {
exit action '@st:stop' :'#AvatarStopState';
state '@st:receive.in0.0' : '#AvatarReceiveState';
transition : '#AvatarTransition' first '@st:receive.in0.0'
then '@st:stop';
state '@st:send.out0.0' : '#AvatarSendState';
transition : '#AvatarTransition' first '@st:send.out0.0'
do action : '#TransitionAction' {
first start;
then assign '$p':= '$make'('$x', '$y');
then assign '$x':= '$getx'('$p');
then done;
} then '@st:random.0';
entry action '@st:start' :'#AvatarStartState' = '#AvatarStartState'(
'@request' = {
'#TrivialRequest'('@delay' = '#bound_random'(1, '$p'.'x'))
}
);
transition : '#AvatarTransition' first '@st:start'
do action : '#TransitionAction' {
first start;
then assign '$x':= 1;
then assign '$b':= true;
then assign '$p'::'x':= '$x';
then done;
} then '@st:presend.out0.0';
state '@st:presend.out0.0' : '#AvatarPreSendState' = '#AvatarPreSendState' (
'@request' = {
'#SendRequest'(
'@channel'= '@sig:out0',
'@payload' = '@MSG:B0.out0'(
'$x',
'$p',
'$b' )
)
}
);
transition : '#AvatarTransition' first '@st:presend.out0.0' then '@st:send.out0.0';
state '@st: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 '@st:random.0'
do action : '#TransitionAction' {
first start;
then action = '$foo'('$x', '$p', '$b');
then done;
} then '@st:prereceive.in0.0';
state '@st:prereceive.in0.0' : '#AvatarPreReceiveState' = '#AvatarPreReceiveState' (
'@request' = {
'#ReceiveRequest'(
'@channel'= '@sig:in0'
)
}
);
transition : '#AvatarTransition' first '@st:prereceive.in0.0'
do action : '#ReceiveAction' {
item '@msg' : '@MSG:B0.in0' = '@payload' as '@MSG:B0.in0';
first start;
then assign '$x' := '@msg'.'x';
then assign '$p' := '@msg'.'p';
then assign '$b' := '@msg'.'b';
then done;
} then '@st:receive.in0.0';
}
}
// Block '@blk:B1'=============
part '@blk:B1' : '#AvatarBlock' {
// Attributes ---------------------
attribute '$x' : Integer := 0;
attribute '$b' : Boolean := false;
attribute '$p' : '@dt:Point';
// Signals ---------------------
part '@sig:in1' : '#Channel';
part '@sig:out1' : '#Channel';
// state-machine -------------------
exhibit state '@statemachine' : '#AvatarStateMachine' {
state '@st:receive.in1.0' : '#AvatarReceiveState' = '#AvatarReceiveState'(
'@request' = {
'#SendRequest'(
'@channel'= '@sig:out1',
'@payload' = '@MSG:B1.out1'(
'$x',
'$p',
'$b' )
)
}
);
transition : '#AvatarTransition' first '@st:receive.in1.0'
then '@st:send.out1.0';
state '@st:send.out1.0' : '#AvatarSendState';
transition : '#AvatarTransition' first '@st:send.out1.0'
then '@st:stop';
exit action '@st:stop' :'#AvatarStopState';
entry action '@st:start' :'#AvatarStartState' = '#AvatarStartState'(
'@request' = {
'#ReceiveRequest'(
'@channel'= '@sig:in1'
)
}
);
transition : '#AvatarTransition' first '@st:start'
do action : '#ReceiveAction' {
item '@msg' : '@MSG:B1.in1' = '@payload' as '@MSG:B1.in1';
first start;
then assign '$x' := '@msg'.'x';
then assign '$p' := '@msg'.'p';
then assign '$b' := '@msg'.'b';
then done;
} then '@st:receive.in1.0';
}
}
// Block Shortcut Links $$$$$$$$$$$$
}
package AvatarInstance {
private import AvatarGeneral::*;
private import AvatarBlockTypes::*;
private import AvatarCommunication::*;
private import AvatarTransitionServer::*;
// DATATYPES $$$$$$$$$$$$$$$$$$$$$$$$
attribute def '@dt:Point' :> '#AvatarDataType' {
attribute 'x' : Integer default := 0;
attribute 'y' : Integer default := 0;
}
// COMMUNICATIONS $$$$$$$$$$$$$$$$$$$$$$$$
// Relation '@SYN0:B0-B1'=============
part '@SYN0:B0-B1': '#Sync_Rel' = '#Sync_Rel'('@block1' = '@blk:B0', '@block2' = '@blk:B1', '@private'=true;
// Channel '@syn:B0.in0<B1.out1'-------------
part '@syn:B0.in0<B1.out1' : '#Sync' = '#Sync'('@relation' = '@SYN0:B0-B1');
binding : '#InSignalBinding' bind '@blk:B0'.'@sig:in0' = '@syn:B0.in0<B1.out1';
binding : '#OutSignalBinding' bind '@blk:B1'.'@sig:out1' = '@syn:B0.in0<B1.out1';
// Message of signal '@blk:B0'.'@sig:in0'............
part def '@MSG:B0.in0' :> '#InMessage' {
private part '@channel' : '#Channel' = '@syn:B0.in0<B1.out1';
attribute 'x' : Integer;
attribute 'p' : '@dt:Point';
attribute 'b' : Boolean;
}
// Message of signal '@blk:B1'.'@sig:out1'............
part def '@MSG:B1.out1' :> '#OutMessage', '@MSG:B0.in0' {
attribute 'x' redefines 'x';
attribute 'p' redefines 'p';
attribute 'b' redefines 'b';
}
// Channel '@syn:B0.out0>B1.in1'-------------
part '@syn:B0.out0>B1.in1' : '#Sync' = '#Sync'('@relation' = '@SYN0:B0-B1');
binding : '#OutSignalBinding' bind '@blk:B0'.'@sig:out0' = '@syn:B0.out0>B1.in1';
binding : '#InSignalBinding' bind '@blk:B1'.'@sig:in1' = '@syn:B0.out0>B1.in1';
// Message of signal '@blk:B1'.'@sig:in1'............
part def '@MSG:B1.in1' :> '#InMessage' {
private part '@channel' : '#Channel' = '@syn:B0.out0>B1.in1';
attribute 'x' : Integer;
attribute 'p' : '@dt:Point';
attribute 'b' : Boolean;
}
// Message of signal '@blk:B0'.'@sig:out0'............
part def '@MSG:B0.out0' :> '#OutMessage', '@MSG:B1.in1' {
attribute 'x' redefines 'x';
attribute 'p' redefines 'p';
attribute 'b' redefines 'b';
}
// BLOCKS $$$$$$$$$$$$$$$$$$$$$$$$
// Block '@blk:B0'=============
part '@blk:B0' : '#AvatarBlock' {
// Attributes ---------------------
attribute '$x' : Integer default := 0;
attribute '$b' : Boolean default := false;
attribute '$p' : '@dt:Point';
attribute '$y' : Integer default := 0;
// Methods ---------------------
calc '$make': '#AvatarCalcMethod' {
attribute 'x' : Integer;
attribute 'y' : Integer;
return : '@dt:Point';
}
calc '$getx': '#AvatarCalcMethod' {
attribute 'p' : '@dt:Point';
return : Integer;
}
action '$foo': '#AvatarVoidMethod' {
attribute 'x' : Integer;
attribute 'p' : '@dt:Point';
attribute 'b' : Boolean;
}
// Signals ---------------------
part '@sig:in0' : '#Channel';
part '@sig:out0' : '#Channel';
// state-machine -------------------
exhibit state '@statemachine' : '#AvatarStateMachine' {
exit action '@st:stop' :'#AvatarStopState';
state '@st:receive.in0.0' : '#AvatarReceiveState';
transition : '#AvatarTransition' first '@st:receive.in0.0'
then '@st:stop';
state '@st:send.out0.0' : '#AvatarSendState';
transition : '#AvatarTransition' first '@st:send.out0.0'
do action : '#TransitionAction' {
first start;
then assign '$p':= '$make'('$x', '$y');
then assign '$x':= '$getx'('$p');
then done;
} then '@st:random.0';
entry action '@st:start' :'#AvatarStartState' = '#AvatarStartState'(
'@request' = {
'#TrivialRequest'('@delay' = '#bound_random'(1, '$p'.'x'))
}
);
transition : '#AvatarTransition' first '@st:start'
do action : '#TransitionAction' {
first start;
then assign '$x':= 1;
then assign '$b':= true;
then assign '$p'::'x':= '$x';
then done;
} then '@st:presend.out0.0';
state '@st:presend.out0.0' : '#AvatarPreSendState' = '#AvatarPreSendState' (
'@request' = {
'#SendRequest'(
'@channel'= '@sig:out0',
'@payload' = '@MSG:B0.out0'(
'$x',
'$p',
'$b' )
)
}
);
transition : '#AvatarTransition' first '@st:presend.out0.0' then '@st:send.out0.0';
state '@st: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 '@st:random.0'
do action : '#TransitionAction' {
first start;
then action = '$foo'('$x', '$p', '$b');
then done;
} then '@st:prereceive.in0.0';
state '@st:prereceive.in0.0' : '#AvatarPreReceiveState' = '#AvatarPreReceiveState' (
'@request' = {
'#ReceiveRequest'(
'@channel'= '@sig:in0'
)
}
);
transition : '#AvatarTransition' first '@st:prereceive.in0.0'
do action : '#ReceiveAction' {
item '@msg' : '@MSG:B0.in0' = '@payload' as '@MSG:B0.in0';
first start;
then assign '$x' := '@msg'.'x';
then assign '$p' := '@msg'.'p';
then assign '$b' := '@msg'.'b';
then done;
} then '@st:receive.in0.0';
}
}
// Block '@blk:B1'=============
part '@blk:B1' : '#AvatarBlock' {
// Attributes ---------------------
attribute '$x' : Integer := 0;
attribute '$b' : Boolean := false;
attribute '$p' : '@dt:Point';
// Signals ---------------------
part '@sig:in1' : '#Channel';
part '@sig:out1' : '#Channel';
// state-machine -------------------
exhibit state '@statemachine' : '#AvatarStateMachine' {
state '@st:receive.in1.0' : '#AvatarReceiveState' = '#AvatarReceiveState'(
'@request' = {
'#SendRequest'(
'@channel'= '@sig:out1',
'@payload' = '@MSG:B1.out1'(
'$x',
'$p',
'$b' )
)
}
);
transition : '#AvatarTransition' first '@st:receive.in1.0'
then '@st:send.out1.0';
state '@st:send.out1.0' : '#AvatarSendState';
transition : '#AvatarTransition' first '@st:send.out1.0'
then '@st:stop';
exit action '@st:stop' :'#AvatarStopState';
entry action '@st:start' :'#AvatarStartState' = '#AvatarStartState'(
'@request' = {
'#ReceiveRequest'(
'@channel'= '@sig:in1'
)
}
);
transition : '#AvatarTransition' first '@st:start'
do action : '#ReceiveAction' {
item '@msg' : '@MSG:B1.in1' = '@payload' as '@MSG:B1.in1';
first start;
then assign '$x' := '@msg'.'x';
then assign '$p' := '@msg'.'p';
then assign '$b' := '@msg'.'b';
then done;
} then '@st:receive.in1.0';
}
}
// Block Shortcut Links $$$$$$$$$$$$
}
package AvatarInstance {
private import AvatarGeneral::*;
private import AvatarBlockTypes::*;
private import AvatarCommunication::*;
private import AvatarTransitionServer::*;
// DATATYPES $$$$$$$$$$$$$$$$$$$$$$$$
attribute def '@dt:Point' :> '#AvatarDataType' {
attribute 'x' : Integer default := 0;
attribute 'y' : Integer default := 0;
}
// COMMUNICATIONS $$$$$$$$$$$$$$$$$$$$$$$$
// Relation '@SYN0:B0-B1'=============
part '@SYN0:B0-B1': '#Sync_Rel' = '#Sync_Rel'('@block1' = '@blk:B0', '@block2' = '@blk:B1', '@private'=true);
// Channel '@syn:B0.in0<B1.out1'-------------
part '@syn:B0.in0<B1.out1' : '#Sync' = '#Sync'('@relation' = '@SYN0:B0-B1');
binding : '#InSignalBinding' bind '@blk:B0'.'@sig:in0' = '@syn:B0.in0<B1.out1';
binding : '#OutSignalBinding' bind '@blk:B1'.'@sig:out1' = '@syn:B0.in0<B1.out1';
// Message of signal '@blk:B0'.'@sig:in0'............
part def '@MSG:B0.in0' :> '#InMessage' {
private part '@channel' : '#Channel' = '@syn:B0.in0<B1.out1';
attribute 'x' : Integer;
attribute 'p' : '@dt:Point';
attribute 'b' : Boolean;
}
// Message of signal '@blk:B1'.'@sig:out1'............
part def '@MSG:B1.out1' :> '#OutMessage', '@MSG:B0.in0' {
attribute 'x' redefines 'x';
attribute 'p';
attribute 'b' redefines 'b';
}
// Channel '@syn:B0.out0>B1.in1'-------------
part '@syn:B0.out0>B1.in1' : '#Sync' = '#Sync'('@relation' = '@SYN0:B0-B1');
binding : '#OutSignalBinding' bind '@blk:B0'.'@sig:out0' = '@syn:B0.out0>B1.in1';
binding : '#InSignalBinding' bind '@blk:B1'.'@sig:in1' = '@syn:B0.out0>B1.in1';
// Message of signal '@blk:B1'.'@sig:in1'............
part def '@MSG:B1.in1' :> '#InMessage' {
private part '@channel' : '#Channel' = '@syn:B0.out0>B1.in1';
attribute 'x' : Integer;
attribute 'p' : '@dt:Point';
attribute 'b' : Boolean;
}
// Message of signal '@blk:B0'.'@sig:out0'............
part def '@MSG:B0.out0' :> '#OutMessage', '@MSG:B1.in1' {
attribute 'x' redefines 'x';
attribute 'p' redefines 'p';
attribute 'b' redefines 'b';
}
// BLOCKS $$$$$$$$$$$$$$$$$$$$$$$$
// Block '@blk:B0'=============
part '@blk:B0' : '#AvatarBlock' {
// Attributes ---------------------
attribute '$x' : Integer default := 0;
attribute '$b' : Boolean default := false;
attribute '$p' : '@dt:Point';
attribute '$y' : Integer default := 0;
// Methods ---------------------
calc '$make': '#AvatarCalcMethod' {
attribute 'x' : Integer;
attribute 'y' : Integer;
return : '@dt:Point';
}
calc '$getx': '#AvatarCalcMethod' {
attribute 'p' : '@dt:Point';
return : Integer;
}
action '$foo': '#AvatarVoidMethod' {
attribute 'x' : Integer;
attribute 'p' : '@dt:Point';
attribute 'b' : Boolean;
}
// Signals ---------------------
part '@sig:in0' : '#Channel';
part '@sig:out0' : '#Channel';
// state-machine -------------------
exhibit state '@statemachine' : '#AvatarStateMachine' {
exit action '@st:stop' :'#AvatarStopState';
state '@st:receive.in0.0' : '#AvatarReceiveState';
transition : '#AvatarTransition' first '@st:receive.in0.0'
then '@st:stop';
state '@st:send.out0.0' : '#AvatarSendState';
transition : '#AvatarTransition' first '@st:send.out0.0'
do action : '#TransitionAction' {
first start;
then assign '$p':= '$make'('$x', '$y');
then assign '$x':= '$getx'('$p');
then done;
} then '@st:random.0';
entry action '@st:start' :'#AvatarStartState' = '#AvatarStartState'(
'@request' = {
'#TrivialRequest'('@delay' = '#bound_random'(1, '$p'.'x'))
}
);
transition : '#AvatarTransition' first '@st:start'
do action : '#TransitionAction' {
first start;
then assign '$x':= 1;
then assign '$b':= true;
then assign '$p'::'x':= '$x';
then done;
} then '@st:presend.out0.0';
state '@st:presend.out0.0' : '#AvatarPreSendState' = '#AvatarPreSendState' (
'@request' = {
'#SendRequest'(
'@channel'= '@sig:out0',
'@payload' = '@MSG:B0.out0'(
'$x',
'$p',
'$b' )
)
}
);
transition : '#AvatarTransition' first '@st:presend.out0.0' then '@st:send.out0.0';
state '@st: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 '@st:random.0'
do action : '#TransitionAction' {
first start;
then action = '$foo'('$x', '$p', '$b');
then done;
} then '@st:prereceive.in0.0';
state '@st:prereceive.in0.0' : '#AvatarPreReceiveState' = '#AvatarPreReceiveState' (
'@request' = {
'#ReceiveRequest'(
'@channel'= '@sig:in0'
)
}
);
transition : '#AvatarTransition' first '@st:prereceive.in0.0'
do action : '#ReceiveAction' {
item '@msg' : '@MSG:B0.in0' = '@payload' as '@MSG:B0.in0';
first start;
then assign '$x' := '@msg'.'x';
then assign '$p' := '@msg'.'p';
then assign '$b' := '@msg'.'b';
then done;
} then '@st:receive.in0.0';
}
}
// Block '@blk:B1'=============
part '@blk:B1' : '#AvatarBlock' {
// Attributes ---------------------
attribute '$x' : Integer := 0;
attribute '$b' : Boolean := false;
attribute '$p' : '@dt:Point';
// Signals ---------------------
part '@sig:in1' : '#Channel';
part '@sig:out1' : '#Channel';
// state-machine -------------------
exhibit state '@statemachine' : '#AvatarStateMachine' {
state '@st:receive.in1.0' : '#AvatarReceiveState' = '#AvatarReceiveState'(
'@request' = {
'#SendRequest'(
'@channel'= '@sig:out1',
'@payload' = '@MSG:B1.out1'(
'$x',
'$p',
'$b' )
)
}
);
transition : '#AvatarTransition' first '@st:receive.in1.0'
then '@st:send.out1.0';
state '@st:send.out1.0' : '#AvatarSendState';
transition : '#AvatarTransition' first '@st:send.out1.0'
then '@st:stop';
exit action '@st:stop' :'#AvatarStopState';
entry action '@st:start' :'#AvatarStartState' = '#AvatarStartState'(
'@request' = {
'#ReceiveRequest'(
'@channel'= '@sig:in1'
)
}
);
transition : '#AvatarTransition' first '@st:start'
do action : '#ReceiveAction' {
item '@msg' : '@MSG:B1.in1' = '@payload' as '@MSG:B1.in1';
first start;
then assign '$x' := '@msg'.'x';
then assign '$p' := '@msg'.'p';
then assign '$b' := '@msg'.'b';
then done;
} then '@st:receive.in1.0';
}
}
// Block Shortcut Links $$$$$$$$$$$$
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment