DEUX EXEMPLES DE TELEPHONES CODÉS PAR DES AUTOMATES  SUR LE MÊME SCÉNARIO

- MyPhone v0.0 est codé par un automate deterministe
- MyPhone v1.0 est codé par un autoamte non-déteerministe

- Le pin est tout mot de la forme a^{n+1}.b^{n+1}

TRACES D'EXÉCUTION

TRACE 1.a. RUN OF  MyPhone v0.0  ON SCENARIO: [on ; pin ; b ; a ; a ; b ; enter ; off] 

Process1: USER > KEY [on]
(1)-- on:on -->(0)

* BOOTING

Process1: USER > KEY [pin]
(0)-- pin:pin -->(1001)

* ENTER PIN

Process1: USER > KEY [b]
(1001)-- b:b when stack prefix matches [_] -->(0)

* INCORRECT PIN


TRACE 1.b. DÉTAIL DANS L'INTERPRETE ocaml

-: system_state = {inputs = []; processes = []}

-: system_state =
{inputs = ["on"; "pin"; "b"; "a"; "a"; "b"; "enter"; "off"];
 processes = [{id = 1; state = {node = 1; stack = []}}]}

Process1: USER > KEY [on]
(1)-- on:on -->(0)

* BOOTING

-: system_state =
{inputs = ["pin"; "b"; "a"; "a"; "b"; "enter"; "off"];
 processes = [{id = 1; state = {node = 0; stack = []}}]}

Process1: USER > KEY [pin]
(0)-- pin:pin -->(1001)

* ENTER PIN

-: system_state =
{inputs = ["b"; "a"; "a"; "b"; "enter"; "off"];
 processes = [{id = 1; state = {node = 1001; stack = ["pin"]}}]}

Process1: USER > KEY [b]
(1001)-- b:b when stack prefix matches [_] -->(0)

* INCORRECT PIN

-: system_state =
{inputs = ["a"; "a"; "b"; "enter"; "off"];
 processes = [{id = 1; state = {node = 0; stack = ["pin"]}}]}

-: system_state = {inputs = ["a"; "b"; "enter"; "off"]; processes = []}

-: system_state = {inputs = ["b"; "enter"; "off"]; processes = []}

-: system_state = {inputs = ["enter"; "off"]; processes = []}

-: system_state = {inputs = ["off"]; processes = []}

-: system_state = {inputs = []; processes = []}



TRACE 2. RUN OF  MyPhone v1.0  ON SCENARIO: [on ; pin ; b ; a ; a ; b ; enter ; off] 

-: system_state = {inputs = []; processes = []}

Process1: USER > KEY [on]
(1)-- on:on -->(0)

* BOOTING

Process1: USER > KEY [pin]
(0)-- pin:pin -->(1001)

* ENTER PIN

Process1: USER > KEY [b]
(1001)-- b:b -->(999)

Process1: USER > KEY [a]
(999)-- a:_ -->(999)

Process1: USER > KEY [a]
(999)-- a:_ -->(999)

Process1: USER > KEY [b]
(999)-- b:_ -->(999)

Process1: USER > KEY [enter]
(999)-- enter:enter -->(0)

* INCORRECT PINUSER > KEY [enter]
(999)-- enter:_ -->(999)

Process2: USER > KEY [off]
(999)-- off:_ -->(999)

Process1: USER > KEY [off]
(0)-- off:off -->(1)

* SHUTING DOWN

-: system_state =
{inputs = [];
 processes =
  [{id = 1; state = {node = 1; stack = ["pin"]}};
   {id = 2; state = {node = 999; stack = ["pin"]}}]}
 


TRACE 2.b. DÉTAIL des system_state DANS L'INTERPRÈTE ocaml

L'automate MyPhone v1.0 étant non-déterministe on voit apparaître plusieurs processus.

- : system_state =
{inputs = ["on"; "pin"; "b"; "a"; "a"; "b"; "enter"; "off"];
 processes = [{id = 1; state = {node = 1; stack = []}}]}


Process1: USER > KEY [on]
(1)-- on:on -->(0)

* BOOTING

- : system_state =
{inputs = ["pin"; "b"; "a"; "a"; "b"; "enter"; "off"];
 processes = [{id = 1; state = {node = 0; stack = []}}]}


Process1: USER > KEY [pin]
(0)-- pin:pin -->(1001)

* ENTER PIN

- : system_state =
{inputs = ["b"; "a"; "a"; "b"; "enter"; "off"];
 processes = [{id = 1; state = {node = 1001; stack = ["pin"]}}]}

Process1: USER > KEY [b]
(1001)-- b:b -->(999)

- : system_state =
{inputs = ["a"; "a"; "b"; "enter"; "off"];
 processes = [{id = 1; state = {node = 999; stack = ["pin"]}}]}


Process1: USER > KEY [a]
(999)-- a:_ -->(999)

- : system_state =
{inputs = ["a"; "b"; "enter"; "off"];
 processes = [{id = 1; state = {node = 999; stack = ["pin"]}}]}


Process1: USER > KEY [a]
(999)-- a:_ -->(999)
- : system_state =
{inputs = ["b"; "enter"; "off"];
 processes = [{id = 1; state = {node = 999; stack = ["pin"]}}]}


Process1: USER > KEY [b]
(999)-- b:_ -->(999)

- : system_state =
{inputs = ["enter"; "off"];
 processes = [{id = 1; state = {node = 999; stack = ["pin"]}}]}


Process1: USER > KEY [enter]
(999)-- enter:enter -->(0)

* INCORRECT PIN

Process2: USER > KEY [enter]
(999)-- enter:_ -->(999)

- : system_state =
{inputs = ["off"];
 processes =
  [{id = 1; state = {node = 0; stack = ["pin"]}};
   {id = 2; state = {node = 999; stack = ["pin"]}}]}


Process2: USER > KEY [off]
(999)-- off:_ -->(999)

Process1: USER > KEY [off]
(0)-- off:off -->(1)

* SHUTING DOWN

- : system_state =
{inputs = [];
 processes =
  [{id = 1; state = {node = 1; stack = []}};
   {id = 2; state = {node = 999; stack = []}}]}