4.5 Example

Using the unfolded version of the coloured net 2.2 of the dining philosophers, an example for firing will now be given. Screen displays and excerpts from the session file are shown.

At the start, the initial state and the list of its enabled transitions are outputted:

Fire
Current name options are:
     transition names to be written 

 PL:  1  2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20
 MA:  1  1  1  1  1  0  0  0  0  0  0  0  0  0  0  0  0  0  0  0
enabled:  1.phil1_take_left,  2.phil2_take_left,  3.phil3_take_left,
          4.phil4_take_left,  5.phil5_take_left,  6.phil1_take_right,
          7.phil2_take_right,  8.phil3_take_right,  9.phil4_take_right,
         10.phil5_take_right,
Transition to fire >

By entering <1> , <6> , <11> , and <16> subsequently, you can execute a run-through in which the first philosopher picks up the left and right forks, eats, and puts the forks back. Afterwards, the net is reset to its initial state.

Transition to fire > 1

fired transition:  1.phil1_take_left


 PL:  1  2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20
 MA:  1  1  1  1  0  1  0  0  0  0  0  0  0  0  0  0  0  0  0  0
enabled:  2.phil2_take_left,  3.phil3_take_left,  4.phil4_take_left,
          5.phil5_take_left,  6.phil1_take_right,  7.phil2_take_right,
          8.phil3_take_right,  9.phil4_take_right,
Transition to fire > 6 

fired transition:  6.phil1_take_right


 PL:  1  2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20
 MA:  0  1  1  1  0  1  0  0  0  0  1  0  0  0  0  0  0  0  0  0
enabled:  3.phil3_take_left,  4.phil4_take_left,  5.phil5_take_left,
          7.phil2_take_right,  8.phil3_take_right,  9.phil4_take_right,
         11.phil1_start_eat,
Transition to fire > 11 

fired transition: 11.phil1_start_eat


 PL:  1  2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20
 MA:  0  1  1  1  0  0  0  0  0  0  0  0  0  0  0  1  0  0  0  0
enabled:  3.phil3_take_left,  4.phil4_take_left,  5.phil5_take_left,
          7.phil2_take_right,  8.phil3_take_right,  9.phil4_take_right,
         16.phil1_put_back,
Transition to fire > 16 

fired transition: 16.phil1_put_back


 PL:  1  2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20
 MA:  1  1  1  1  1  0  0  0  0  0  0  0  0  0  0  0  0  0  0  0

Starting in this situation, by entering <cr> repeatedly, the first transition is always fired, and all the philosophers pick up their left fork.

 PL:  1  2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20
 MA:  1  1  1  1  1  0  0  0  0  0  0  0  0  0  0  0  0  0  0  0
enabled:  1.phil1_take_left,  2.phil2_take_left,  3.phil3_take_left,
          4.phil4_take_left,  5.phil5_take_left,  6.phil1_take_right,
          7.phil2_take_right,  8.phil3_take_right,  9.phil4_take_right,
         10.phil5_take_right,
Transition to fire >

fired transition:  1.phil1_take_left


 PL:  1  2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20
 MA:  1  1  1  1  0  1  0  0  0  0  0  0  0  0  0  0  0  0  0  0
enabled:  2.phil2_take_left,  3.phil3_take_left,  4.phil4_take_left,
          5.phil5_take_left,  6.phil1_take_right,  7.phil2_take_right,
          8.phil3_take_right,  9.phil4_take_right,
Transition to fire >

fired transition:  2.phil2_take_left


 PL:  1  2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20
 MA:  0  1  1  1  0  1  1  0  0  0  0  0  0  0  0  0  0  0  0  0
enabled:  3.phil3_take_left,  4.phil4_take_left,  5.phil5_take_left,
          7.phil2_take_right,  8.phil3_take_right,  9.phil4_take_right,
Transition to fire >

fired transition:  3.phil3_take_left


 PL:  1  2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20
 MA:  0  0  1  1  0  1  1  1  0  0  0  0  0  0  0  0  0  0  0  0
enabled:  4.phil4_take_left,  5.phil5_take_left,  8.phil3_take_right,
          9.phil4_take_right,
Transition to fire >

fired transition:  4.phil4_take_left


 PL:  1  2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20
 MA:  0  0  0  1  0  1  1  1  1  0  0  0  0  0  0  0  0  0  0  0
enabled:  5.phil5_take_left,  9.phil4_take_right,
Transition to fire >

fired transition:  5.phil5_take_left


 PL:  1  2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20
 MA:  0  0  0  0  0  1  1  1  1  1  0  0  0  0  0  0  0  0  0  0
 no transition has concession!

Transition to fire >

As indicated by the message above, no transition is enabled any more; the whole net is in a dead state.

In this situation, you can, for example, save the current marking with <W> in a file, and then go back one step with <B> .

Transition to fire >   W

Marking output file > dinner.mar

Marking written to dinner.mar


Transition to fire >   B

previous state


 PL:  1  2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20
 MA:  0  0  0  1  0  1  1  1  1  0  0  0  0  0  0  0  0  0  0  0
enabled:  5.phil5_take_left,  9.phil4_take_right,

ow you can select the other transition and thereby let the fourth philosopher take the missing fork. By entering <cr> , the eating process can start, and afterwards, both forks may be put back again.

Transition to fire > 9 

fired transition:  9.phil4_take_right


 PL:  1  2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20
 MA:  0  0  0  0  0  1  1  1  1  0  0  0  0  1  0  0  0  0  0  0
enabled: 14.phil4_start_eat,
Transition to fire >  

fired transition: 14.phil4_start_eat


 PL:  1  2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20
 MA:  0  0  0  0  0  1  1  1  0  0  0  0  0  0  0  0  0  0  1  0
enabled: 19.phil4_put_back,
Transition to fire >

fired transition: 19.phil4_put_back

 PL:  1  2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20
 MA:  0  0  1  1  0  1  1  1  0  0  0  0  0  0  0  0  0  0  0  0
enabled:  4.phil4_take_left,  5.phil5_take_left,  8.phil3_take_right,
          9.phil4_take_right,
Transition to fire >

Now the philosophers three and five may take another fork. Of course, the fourth philosopher could immediately get hungry again, and unfairly take the forks again, so that the other philosophers would eventually starve.

With <R> , you can quit the run and return to the initial state.

Transition to fire >  R

reset to the initial state


 PL:  1  2  3  4  5  6  7  8  9 10 11 12 13 14 15 16 17 18 19 20
 MA:  1  1  1  1  1  0  0  0  0  0  0  0  0  0  0  0  0  0  0  0
enabled:  1.phil1_take_left,  2.phil2_take_left,  3.phil3_take_left,
          4.phil4_take_left,  5.phil5_take_left,  6.phil1_take_right,
          7.phil2_take_right,  8.phil3_take_right,  9.phil4_take_right,
         10.phil5_take_right,
Transition to fire >

Moreover, with <S> you can at any time inspect the stubborn sets which are used by INA for the stubborn reduction. At the initial marking the stubborn set looks as follows:

Transition to fire >  S

Stubborn set used by stubborn set method is:
       1.phil1_take_left, 10.phil5_take_right,

With <A> , all minimal stubborn sets are displayed; a counter indicates the progression of the calculation:

Transition to fire >  A
                      Candidate nr. 32
All minimal stubborn sets:
   1:  5.phil5_take_left,  9.phil4_take_right,
   2:  4.phil4_take_left,  8.phil3_take_right,
   3:  3.phil3_take_left,  7.phil2_take_right,
   4:  2.phil2_take_left,  6.phil1_take_right,
   5:  1.phil1_take_left, 10.phil5_take_right,

With <Q> , you quit the firing mode and return to the main menu. The initial marking is automatically reset.