avSysML_timerRealNames.sysml

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;
}