1 of 13

100 Prisoners & Light Bulb

​

PRESENTED BY:

Keshav Bulia

PRESENTED TO:

Prof. Paritosh Pandya

​

​

13 Nov 2025

CS771

IIT BOMBAY

2 of 13

1

Problem

2

Solution

3

Code Implementation

4

Properties being verified

Content

3 of 13

Problem

​

​

4 of 13

Solution

5 of 13

6 of 13

7 of 13

8 of 13

9 of 13

Code Implemented

10 of 13

VAR

light : boolean;

current_prisoner : 0..4;

counter_count : 0..4;

light_ever_on : boolean;

​

-- Per-prisoner first-turn-off flags

(only non-counter prisoners)

​

p1_turned_off : boolean;

p2_turned_off : boolean;

p3_turned_off : boolean;

p4_turned_off : boolean;

​

assertion_made : boolean;

11 of 13

next(light) := case

assertion_made : light;

current_prisoner = 0 & !light : TRUE

current_prisoner = 1 & light & !p1_turned_off : FALSE;

current_prisoner = 2 & light & !p2_turned_off : FALSE;

current_prisoner = 3 & light & !p3_turned_off : FALSE;

current_prisoner = 4 & light & !p4_turned_off : FALSE;

TRUE : light; -- otherwise unchanged

esac;

12 of 13

​

next(assertion_made) := case

assertion_made : TRUE; -- latch

counter_count = 4 & all_visited : TRUE;

TRUE : FALSE;

esac;

next(counter_count) := case

assertion_made : counter_count;

current_prisoner = 0 & !light & light_ever_on

& counter_count < 4 : counter_count + 1;

TRUE : counter_count;

esac;

​

next(p1_turned_off) := case

assertion_made : p1_turned_off;

current_prisoner = 1 & light & !p1_turned_off : TRUE;

TRUE : p1_turned_off;

esac;

13 of 13