// This is an outline for the UCLID5 model.
// It will not pass the typechecker or do anything useful.

module System
{
    // Part 1: Variables
    var x : int;

    // Part 2: Initial states
    init {
        x = 3;
    }

    // Part 3: Transitions
    next(x) :=
        case
            // Action A
            is_action_A : 2 * x;
            // Action B
            is_action_B : x + 1;
            // Default case to handle stability when no actions are taken
            TRUE        : x;
        esac;

    // Part 4: System description

    // Part 5: Proof script
    invariant prop1 : (x >= 3);
    control
    {
        // Part 6: Bounded model checking
        bmc[proof] = unroll(2);
        // Part 7: Counterexample generation
        bmc.print_cex(x);
    }
}
