target C;

reactor Controller {
    output out:int;
    reaction(startup) -> out {=        
        lf_set(out, 1);
    =}
}

reactor Vision {
    
    input in:int;
    output out:int;
    state ramp:int = 0;
    
    reaction(in) -> out {=
        if (self->ramp == 1) {
            lf_set(out, 0); // 0 = Do not open.
        } else {
            lf_set(out, 1); // 1 = Open.
        }
    =}
}

reactor Door {
    input in:int;
    state doorOpen:int;
    reaction(in) {=
        if (in->value == 1)
            self->doorOpen = 1; // Open
        else if (in->value == 0)
            self->doorOpen = 0; // Closed
    =}
}

//@property(name="vision_works", tactic="bmc", spec="((AircraftDoor_vision_ramp == 0) ==> (G[0 sec](AircraftDoor_door_reaction_0 ==> (AircraftDoor_door_doorOpen == 1))))", expect=true)
@maude(analysis="ltl", goal="(ramp in vision == 0) -> [] ((door. 1 invoked) -> (doorOpen in door == 1))", timeBound=0)
main reactor AircraftDoor {
    controller	= new Controller();
    vision		= new Vision();
    door		= new Door();
    controller.out -> vision.in;
    vision.out -> door.in;
}
