byte person0 =7, person1 =2, person2 =6, person3 =5, person4;
byte conflictA0 =0, conflictA1 =0, conflictA2 =0, conflictA3 =0, conflictA4;
byte conflictB0 =0, conflictB1 =0, conflictB2 =0, conflictB3 =0, conflictB4;
byte not_alone0 =0, not_alone1 =0, not_alone2 =0, not_alone3 =0, not_alone4;
byte at=0;
byte inA=0;
byte inB=0;
byte inNew=0;
byte alone=0;
byte i=0;

active proctype Elevator() {
q: if
:: person0==0 && person1==0 && person2==0 && person3==0; goto out;
::  atomic {person0==at && inNew<4 && (conflictA0==0 || inB==0) && (conflictB0==0 || inA==0) && (not_alone0==0 || inNew>0);person0 = 255;inNew = inNew+1;inA = inA+conflictA0;inB = inB+conflictB0;alone = alone+not_alone0;}  goto q;
::  atomic {person1==at && inNew<4 && (conflictA1==0 || inB==0) && (conflictB1==0 || inA==0) && (not_alone1==0 || inNew>0);person1 = 255;inNew = inNew+1;inA = inA+conflictA1;inB = inB+conflictB1;alone = alone+not_alone1;}  goto q;
::  atomic {person2==at && inNew<4 && (conflictA2==0 || inB==0) && (conflictB2==0 || inA==0) && (not_alone2==0 || inNew>0);person2 = 255;inNew = inNew+1;inA = inA+conflictA2;inB = inB+conflictB2;alone = alone+not_alone2;}  goto q;
::  atomic {person3==at && inNew<4 && (conflictA3==0 || inB==0) && (conflictB3==0 || inA==0) && (not_alone3==0 || inNew>0);person3 = 255;inNew = inNew+1;inA = inA+conflictA3;inB = inB+conflictB3;alone = alone+not_alone3;}  goto q;
::  atomic {person0==255 && (inNew>2 || (alone-not_alone0==0));person0 = at;inNew = inNew-1;inA = inA-conflictA0;inB = inB-conflictB0;alone = alone-not_alone0;}  goto q;
::  atomic {person1==255 && (inNew>2 || (alone-not_alone1==0));person1 = at;inNew = inNew-1;inA = inA-conflictA1;inB = inB-conflictB1;alone = alone-not_alone1;}  goto q;
::  atomic {person2==255 && (inNew>2 || (alone-not_alone2==0));person2 = at;inNew = inNew-1;inA = inA-conflictA2;inB = inB-conflictB2;alone = alone-not_alone2;}  goto q;
::  atomic {person3==255 && (inNew>2 || (alone-not_alone3==0));person3 = at;inNew = inNew-1;inA = inA-conflictA3;inB = inB-conflictB3;alone = alone-not_alone3;}  goto q;
:: at = 0; goto q;
:: at = 1; goto q;
:: at = 2; goto q;
:: at = 3; goto q;
:: at = 4; goto q;
:: at = 5; goto q;
:: at = 6; goto q;
:: at = 7; goto q;
fi;
out: skip; }

never
{
again:
  if
  ::true; goto again;
  ::person0==0 && person1==0 && person2==0 && person3==0;
  fi;
}