module Communication {
    type port gt1 message {
        inout integer
    }
    

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

    function f_Message() 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 ct1 peer;
        var ct1 correspondent;
        //peer := ct1.create;
        
        g1.send(v_s1);
        g1.send(v_s2);
        g1.send(v_s2) to peer;

        g1.receive(v_s1);
        g1.receive(v_s2);
        g1.receive(v_s2) from peer;
        
        //assignments
        if (1 > 0) {
            g1.receive(v_s2) -> value v_s4;
            g1.receive(v_s2) -> sender correspondent;

            g1.send(v_s4) to correspondent;
        }

        g1.send(v_s4) to correspondent;

        //triggers
        if (2 > 1) {
            g1.trigger(v_s1) from peer;
            g1.trigger(v_s2) -> value v_s4;
            g1.trigger(v_s2) -> sender correspondent;

            g1.send(v_s4) to correspondent;
        }
        
        g1.send(v_s4) to correspondent;

        //checks
        if (3 > 1) {
            g1.check(receive(v_s1) from peer);
            g1.check(receive(v_s2) -> value v_s4);
            g1.check(receive(v_s2) -> sender correspondent);

            g1.send(v_s4) to correspondent;
        }

        g1.send(v_s4) to correspondent;
        
        g1.checkstate(v_s1);
        g1.checkstate(v_s2);
        
        g1.halt;
        g1.clear;
        //ambiguity
//        g1.start;
//        g1.stop;

    }

    signature s_s1(integer p1, integer p2) return integer exception (s_e1);

    signature s_e1();

    function f_Procedure (integer p1, integer p2) 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;

        g1.call(s_s1:{v_s1, v_s2}, nowait);

        if (v_s2 > 1) {
            g1.getreply(s_s1:{v_s1, v_s2}) -> value v_s3 param (v_s5);
            v_s4 := v_s5;
            v_s4 := v_s3;
        }        

        if (v_s2 > 1) {
            g1.getcall(s_s1:{v_s1, v_s2}) from peer -> param (v_s5) sender peer;
            peer.kill;
            v_s4 := v_s5;
        }

        if (v_s2 > 1) {
            g1.reply(s_s1:{v_s1, v_s2}) to peer;
            g1.reply(s_s1:{v_s1, v_s2} value v_s1);
        }

        if (v_s2 > 1) {
            g1.raise(s_e1, v_s2) to peer;
            g1.raise(s_e1, v_s1);
        }

        if (v_s2 > 1) {
            g1.catch(s_e1, v_s2) -> sender correspondent;
            g1.catch(s_e1, v_s1) from peer;
            correspondent.kill;
        }
        
        g1.call(s_s1:{v_s1, v_s2}) to peer {
            [v_s2 > v_s1] g1.getreply(s_s1:{v_s1, v_s2}) -> value v_s3 param (v_s5) {
                //should be yes?
                v_s4 := v_s3;
                v_s4 := v_s5;
                //is this a yes? or a maybe outside
                v_s3 := 1;
                v_s4 := v_s3;
            }
            [] g1.getreply(s_s1:{v_s1, v_s3}) from peer {
                //should be no
                v_s4 := v_s3;
                //is this a yes? or a maybe outside
                v_s3 := 1;
            }
            [] g1.catch(s_e1,v_s1) -> sender correspondent {
                //is this a yes? or a maybe
                v_s3 := 1;
                correspondent.kill;
            }
            [] g1.catch(timeout) {
                //is this a yes? or a maybe
                v_s3 := 1;
            }
        };
        
        //yes
        v_s4 := v_s3;
        //no
        v_s4 := v_s5;
        //no
        correspondent.kill;
        
    }    
}