byte person0=0, person1=1, person2=2, person3=3, person4=4, person5=0, person6=3;
byte conflictA0 =1, conflictA1 =0, conflictA2 =0, conflictA3 =1, conflictA4 =1, conflictA5 =0, conflictA6 =0;
byte conflictB0 =0, conflictB1 =1, conflictB2 =1, conflictB3 =0, conflictB4 =0, conflictB5 =1, conflictB6 =0;
byte not_alone0 =1, not_alone1 =1, not_alone2 =0, not_alone3 =0, not_alone4 =0, not_alone5 =0, not_alone6 =0;
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 && person4==0 && person5==0 && person6==0; goto out;
::  atomic {person0==at && inNew<3 && (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<3 && (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<3 && (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<3 && (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 {person4==at && inNew<3 && (conflictA4==0 || inB==0) && (conflictB4==0 || inA==0) && (not_alone4==0 || inNew>0);person4 = 255;inNew = inNew+1;inA = inA+conflictA4;inB = inB+conflictB4;alone = alone+not_alone4;}  goto q;
::  atomic {person5==at && inNew<3 && (conflictA5==0 || inB==0) && (conflictB5==0 || inA==0) && (not_alone5==0 || inNew>0);person5 = 255;inNew = inNew+1;inA = inA+conflictA5;inB = inB+conflictB5;alone = alone+not_alone5;}  goto q;
::  atomic {person6==at && inNew<3 && (conflictA6==0 || inB==0) && (conflictB6==0 || inA==0) && (not_alone6==0 || inNew>0);person6 = 255;inNew = inNew+1;inA = inA+conflictA6;inB = inB+conflictB6;alone = alone+not_alone6;}  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;
::  atomic {person4==255 && (inNew>2 || (alone-not_alone4==0));person4 = at;inNew = inNew-1;inA = inA-conflictA4;inB = inB-conflictB4;alone = alone-not_alone4;}  goto q;
::  atomic {person5==255 && (inNew>2 || (alone-not_alone5==0));person5 = at;inNew = inNew-1;inA = inA-conflictA5;inB = inB-conflictB5;alone = alone-not_alone5;}  goto q;
::  atomic {person6==255 && (inNew>2 || (alone-not_alone6==0));person6 = at;inNew = inNew-1;inA = inA-conflictA6;inB = inB-conflictB6;alone = alone-not_alone6;}  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;
fi;
out: skip; }

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