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