/*
 * Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 */

import <std_connector.camkes>;

procedure P {
    int echo(in int x);
}

component Foo {
    control;
    uses P outgoing;
    provides P incoming;
}

component Bar {
    provides P incoming;
    uses P outgoing;
}

assembly {
    composition {
        component Foo foo;
        component Bar bar;

        connection seL4RPCCall conn1(from foo.outgoing, to bar.incoming);
        connection seL4RPCCall conn2(from bar.outgoing, to foo.incoming);
    }
}