module Behaviour {
    type port gt1 message {
        inout integer
    }

    type component ct1 {
        var integer cv_s0;
        port gt1 g1 ;
        port gt1 g2 ;
    }

    function f_Alt() runs on ct1 {
        var integer v_s0;
        var integer v_s1;
        var integer v_s2 := 1;
        var integer v_s3;
        var integer v_s4;
        var integer v_s5;
        var ct1 peer;
        var ct1 correspondent;
        timer t;
        //peer := ct1.create;
        
        alt { 
            []g1.receive(v_s1) -> sender correspondent {
                v_s0 := v_s3;
                v_s0 := v_s5;
                correspondent.kill
            }
            []g1.receive(v_s2) -> value v_s4 {
                //is s4 visible outside?
                v_s0 := v_s4;
                v_s0 := v_s5;
            }
            []g1.receive(v_s2) from peer {
                v_s0 := v_s4;
            }
            []t.timeout {
                v_s0 := v_s4;
            }
            []as_Base(v_s1, v_s2) {
                v_s0 := v_s4;
            }
            [else] {
                v_s0 := v_s4;
                v_s0 := v_s5;
            }
        }
        v_s1 := v_s0;
        v_s1 := v_s4;        
        var integer v_sX := 0;
    }

    altstep as_Base(integer p1, integer p2) runs on ct1 {
        
    }
    
    function f_Interleaved() runs on ct1 {
        var integer v_s0;
        var integer v_s1;
        var integer v_s2 := 1;
        var integer v_s3;
        var integer v_s4;
        var integer v_s5;
        var ct1 peer;
        var ct1 correspondent;
        
        interleave { 
            []g1.receive(v_s1) -> sender correspondent {
                v_s0 := v_s3;
                v_s0 := v_s5;
                correspondent.kill
            }
            []g1.receive(v_s2) -> value v_s4 {
                //is s4 visible outside?
                v_s0 := v_s4;
                v_s0 := v_s5;
            }
        }

        alt { 
            []g1.receive(v_s1) -> sender correspondent {
                correspondent.kill
            }
            []g1.receive(v_s2) -> sender correspondent  { 
                correspondent.kill
            }
        }
        correspondent.kill

    }

    function f_Altstep() runs on ct1 {
        var integer v_s0;
        var integer v_s1;
        var integer v_s2 := 1;
        var integer v_s3;
        var integer v_s4;
        var integer v_s5;
        
        var default d1;
        var default d2;
        var default d3 := activate(as_Base(v_s1, v_s2));
        
        d2 := activate(as_Base(v_s1, v_s2));
        
        deactivate(d1);
        deactivate(d2);
        deactivate(d3);
        
        as_Base(v_s1, v_s2); //check why not covered
        v_s0 := v_s1;
 
    }

    function f_Function() runs on ct1 {
        var integer v_s0;
        var integer v_s1;
        var integer v_s2 := 1;
        f_Called(v_s1, v_s2);
        v_s0 := f_Called(v_s1, v_s2);
        var integer v_s3 := f_Called(v_s1, v_s2);
    }

    function f_Called(integer p1, integer p2) runs on ct1 {
    }    

    function f_GoToLabel(integer p1, integer p2) runs on ct1 {
        //not supported
        label l1;
        
        if (p1 > p2) {
            goto l1;
        }
    }    

    function f_Testcase(integer p1, integer p2) runs on ct1 {
        var integer v_s1;
        var integer v_s2 := 1;
        var integer v_s3;
        var integer v_s4;
        var verdicttype v_e0;
        
        execute(tc_E1(v_s1, v_s2),v_s3)
        setverdict(v_e0); //not checked?!
        v_e0 := execute(tc_E1(v_s1, v_s2),v_s3)
        var verdicttype v_e1 := execute(tc_E1(v_s1, v_s2),v_s3)
        setverdict(v_e0); //not checked?!
        execute(tc_E1(v_s1, v_s2),v_s3,v_s4)
    }

    testcase tc_E1(integer p1, integer p2) runs on ct1 {
    }

    
}