Concurrent Elevator Property Specifications as QREs

This page describes the concurrent elevator properties as Quantified Regular Expressions ( QREs ). For other property specification formalisms, click on the name of the property.

Direction of Movement property

for events { {directionup=t}, {directionup=f}, 
             {directionupis=t}, {directionupis=f}, 
             {ordered_to_move_up}, {ordered_to_move_down}}

show no executions satisfy

.*;
{directionup=f};
[-{directionup=t}]*;
{ordered_to_move_up};
.*

Not Move With Doors Open property

for events { {open_doors}, {close_doors}, {ordered_to_move} }

show no executions satisfy

.*;
{open_doors};
[-{close_doors}]*;
{ordered_to_move};
.*

Opens Doors When Ordered To Stop property

for events { {not_moving}, {open_doors}, {ordered_to_move}, 
             {ordered_to_stop}, {reporting_approach} }

show no executions satisfy

.*;
{ordered_to_stop};
[-{open_doors}]*;
({ordered_to_move}|{reporting_approach});
.*

Back to Concurrent Elevator

Back to main