// Purpose: test that groups can be used as macro parameters
// Description: A single module which defines a group of integers, containing 0,1,2 and 3. The module also defines the macro allGreaterThan which takes two input parameters: a group of integers, and an integer i. allGreaterThan returns true if all the members of the group are greater than the integer i. The module has two properties: one which checks that all members of the group are greater than 2, and one taht checks all members of the group are greater than -1.
// Expectation: one property should pass and the other should fail
// Validation:

module main {
    group myGroup : integer = {0, 1, 2, 3};

    define allGreaterThan(grp : group(integer), i : integer) : boolean = finite_forall (int : integer) in grp :: int > i;

    property test1 : allGreaterThan(myGroup, -1); //Should pass
    property test2 : allGreaterThan(myGroup, 2); //Should fail

    init {
    }

    next {
    }

    control {
        v = unroll(0);
        check;
        print_results;
    }
}
