(* * ledit ocaml * #use "main.ml";; * *) (* COUNTER *) let _id = ref 0 ;; let newid () = begin _id:=!_id + 1 ; !_id end (* EVENT *) type com_event = | Decrocher | Raccrocher | Reprise | Reject type mp3_event = | Play | Pause | Stop type os_event = | Appel | Music type phone_event = | On | Off type vol_event = | Inc | Dec type event = | Epsilon | OS_event of os_event | Mp3_event of mp3_event | Com_event of com_event | Vol_event of vol_event | Phone_event of phone_event (* UNUSED *) | Key_pressed of char (* STATE *) type com_state = | RINGING | COMMUNICATION | SUSPENDED | MULTIPLE_CALL type mp3_state = | PLAY | PAUSE type os_state = | BOOTING | RUNNING type vol_state = | MUTE | NORMAL | HIGH type phone_state = | ON | SHUTDOWN | OFF type keyboard_state = | REACTIVE type state = | Killed_state | KB_state of keyboard_state | OS_state of os_state | Mp3_state of mp3_state | Com_state of com_state | Vol_state of vol_state | Phone_state of phone_state (* AUTOMATA *) type symbol = event list type transition = state * event * action * state and automata = { name: string ; initial_state: state ; transitions: transition list} and action = | Nop | Create of automata | Send of event list (* SYSTEM *) type origin = | Key of char (* key pressed *) | Ext of char (* external event *) | Int of string (* internal event emitted by ... *) type interaction = origin * event list type process = { aut: string ; id: int ; current_state: state } type system = { input: interaction list ; processes: process list } (* STATES OF AN AUTOMATON *) type 't set = 't list let rec (add: 't -> 't set -> 't set) = fun t' set' -> match set' with | [] -> [t'] | t::set -> if t=t' then set' else t::(add t' set) let (union: 't set -> 't set -> 't set) = List.fold_right add ;; let rec (all_states: transition list -> state list) = List.fold_left (fun states (src,_,_,tgt) -> add src (add tgt states)) [] ;; (* AUTOMATIC COMPLETION OF AN AUTOMATION *) let (add_killing_transitions: transition list -> transition list) = fun transitions -> let killing_transitions = List.map (fun state -> (state, Phone_event(Off), Nop, Killed_state) ) (all_states transitions) in transitions @ killing_transitions (* MODELISATION OF A CELL PHONE *) let a_kb = (* UNUSED, makes the demo too heavy to follow *) { name = "keyboard" ; initial_state = KB_state(REACTIVE) ; transitions = add_killing_transitions [ ( KB_state(REACTIVE), Key_pressed('f'), Send [ Phone_event(Off) ], KB_state(REACTIVE) ) ; ( KB_state(REACTIVE), Key_pressed('+'), Send [ Vol_event(Inc) ], KB_state(REACTIVE) ) ; ( KB_state(REACTIVE), Key_pressed('-'), Send [ Vol_event(Dec) ], KB_state(REACTIVE) ) ; ( KB_state(REACTIVE), Key_pressed('d'), Send [ Com_event(Decrocher) ], KB_state(REACTIVE) ) ; ( KB_state(REACTIVE), Key_pressed('r'), Send [ Com_event(Raccrocher) ; Com_event(Reject) ; Com_event(Reprise) ], KB_state(REACTIVE) ) ; ( KB_state(REACTIVE), Key_pressed('m'), Send [ OS_event(Music) ], KB_state(REACTIVE) ) ; ( KB_state(REACTIVE), Key_pressed('p'), Send [ Mp3_event(Play) ; Mp3_event(Pause) ], KB_state(REACTIVE) ) ; ( KB_state(REACTIVE), Key_pressed('s'), Send [ Mp3_event(Stop) ], KB_state(REACTIVE) ) ] } let a_com = { name = "communication" ; initial_state = Com_state(RINGING) ; transitions = add_killing_transitions [ ( Com_state(RINGING), Com_event(Reject), Nop, Killed_state ) ; ( Com_state(RINGING), Com_event(Decrocher), Nop, Com_state(COMMUNICATION) ) ; ( Com_state(COMMUNICATION), OS_event(Appel), Nop, Com_state(MULTIPLE_CALL) ) ; ( Com_state(COMMUNICATION), Com_event(Raccrocher), Nop, Killed_state ) ; ( Com_state(MULTIPLE_CALL), Com_event(Reject), Nop, Com_state(COMMUNICATION) ) ; ( Com_state(MULTIPLE_CALL), Com_event(Decrocher), Nop, Com_state(SUSPENDED) ) ; ( Com_state(SUSPENDED), Com_event(Reprise), Nop, Com_state(COMMUNICATION) ) ] } let a_vol = { name = "volume manager" ; initial_state = Vol_state(NORMAL) ; transitions = add_killing_transitions [ ( Vol_state(NORMAL), Vol_event(Inc), Nop, Vol_state(HIGH) ) ; ( Vol_state(HIGH), Vol_event(Dec), Nop, Vol_state(NORMAL) ) ; ( Vol_state(NORMAL), Vol_event(Dec), Send [Mp3_event(Pause)] , Vol_state(MUTE) ) ; ( Vol_state(MUTE), Vol_event(Inc), Nop, Vol_state(NORMAL) ) ] } let a_mp3 = { name = "mp3 player" ; initial_state = Mp3_state(PLAY) ; transitions = add_killing_transitions [ ( Mp3_state(PLAY), Mp3_event(Pause), Nop, Mp3_state(PAUSE) ) ; ( Mp3_state(PLAY), Mp3_event(Stop), Nop, Killed_state ) ; ( Mp3_state(PAUSE), Mp3_event(Play), Nop, Mp3_state(PLAY) ) ; ( Mp3_state(PAUSE), Mp3_event(Stop), Nop, Killed_state ) ; ( Mp3_state(PLAY), Com_event(Decrocher), Nop, Mp3_state(PAUSE) ) ; ( Mp3_state(PLAY), OS_event(Music), Nop, Mp3_state(PAUSE) ) ] } let a_os = { name = "os" ; initial_state = OS_state(BOOTING) ; transitions = add_killing_transitions [ ( OS_state(BOOTING), Epsilon, Create(a_vol), OS_state(RUNNING) ) ; ( OS_state(RUNNING), OS_event(Appel), Create(a_com), OS_state(RUNNING) ) ; ( OS_state(RUNNING), OS_event(Music), Create(a_mp3), OS_state(RUNNING) ) ] } let a_phone = { name = "phone" ; initial_state = Phone_state(OFF) ; transitions = [ ( Phone_state(OFF), Phone_event(On), Create(a_os), Phone_state(ON) ) ; ( Phone_state(ON) , Phone_event(Off), Nop, Phone_state(SHUTDOWN) ) ; ( Phone_state(SHUTDOWN) , Epsilon , Nop, Phone_state(OFF) ) ] } (* THE SYSTEM *) let _the_system = [ a_phone ; a_kb ; a_os ; a_vol ; a_mp3 ; a_com ] (* CHAR -> INTERACTION *) (* On a phone the same key often played several roles, thus it corresponds to several events. * For instance, it is very common that the same key controls play/pause of a music player. *) let (interaction_associated_to: char -> interaction) = fun c -> match c with | '#' -> (Ext c ,[ OS_event(Appel) ]) | '+' -> (Key c, [ Vol_event(Inc) ]) | '-' -> (Key c, [ Vol_event(Dec) ]) | 'd' -> (Key c, [ Com_event(Decrocher) ]) | 'f' -> (Key c, [ Phone_event(Off) ]) | 'o' -> (Key c, [ Phone_event(On) ]) | 'm' -> (Key c, [ OS_event(Music) ]) | 'p' -> (Key c, [ Mp3_event(Play) ; Mp3_event(Pause) ]) | 'r' -> (Key c, [ Com_event(Raccrocher) ; Com_event(Reject) ; Com_event(Reprise) ]) | 's' -> (Key c, [ Mp3_event(Stop) ]) | _ -> (Int "", []) (* FONCTIONNEMENT *) module SystemState = (struct type t = system let empty = { input = [] ; processes = [] } let single process = { empty with processes = [ process ] } let compare_process (aut1,id1) (aut2,id2) = match compare aut1 aut2 with | 0 -> ~- (compare id1 id2) | v -> v let (update: system -> system -> system) = fun system1 system2 -> { input = system1.input @ system2.input ; processes = (List.sort (fun p1 p2 -> (compare_process (p1.aut,p1.id) (p2.aut,p2.id))) (union system1.processes system2.processes)) } end) module Process = (struct let (start: automata -> process) = fun aut -> { aut = aut.name ; id = newid () ; current_state = aut.initial_state } let (transitions_of: process -> transition list) = fun process -> match List.filter (fun aut -> aut.name = process.aut) _the_system with | [] -> [] | aut::_ -> aut.transitions let (execute_one: process -> transition -> system) = fun process (_,_,act,tgt) -> match act with | Nop -> { SystemState.empty with processes = [ { process with current_state = tgt} ] } | Send(events) -> { SystemState.empty with input = [ (Int process.aut, events) ] ; processes = [ { process with current_state = tgt } ] } | Create(aut) -> { SystemState.empty with processes = [ start aut ; { process with current_state = tgt} ] } let (execute_all_enabled: process -> transition list -> system) = fun process transitions -> match transitions with | [] -> SystemState.single process | transitions -> List.fold_left (fun system transition -> SystemState.update (execute_one process transition) system) SystemState.empty transitions let (move_on: process -> symbol -> system) = fun process symbol -> if process.current_state = Killed_state then SystemState.empty else let current_transitions = List.filter (fun (src,_,_,_) -> src=process.current_state) (transitions_of process) in let enabled_transitions = List.filter (fun (_,evt,_,_) -> evt=Epsilon || List.mem evt symbol) current_transitions in execute_all_enabled process enabled_transitions end) module System = (struct let empty = SystemState.empty let (move_each_process_on: symbol -> system -> system) = fun symbol system -> List.fold_left (fun system process -> SystemState.update (Process.move_on process symbol) system) { system with processes = [] } system.processes let rec (epsilon_transitions: system -> system) = fun system -> let system' = move_each_process_on [Epsilon] system in if system = system' then system else epsilon_transitions system' let (one_transition: system -> system) = fun system -> match system.input with | [] -> system | (_,symbol)::others -> move_each_process_on symbol { system with input = others } let (one_step: system -> system) = fun system -> (* FIXME epsilon_transitions (one_transition (epsilon_transitions system)) *) one_transition system end) (* RUN STEP BY STEP *) let _sys = ref System.empty ;; let (load: char list -> system) = fun scenario -> begin _id := 0 ; _sys:= { System.empty with processes = [ Process.start a_phone ] ; input = List.map interaction_associated_to scenario } ; !_sys end let (step: unit -> system) = fun () -> begin _sys:= System.one_step !_sys ; !_sys end (* TEST *) let scenario1 = [ 'o' ; '.' ; 'm' ; 'm' ; 'p' ; 'p' ; 'p' ; '+' ; '-' ; '-' ; '-' ; '+' ; 'p' ; 's' ; 'f' ; '.' ] ;; let scenario2 = [ 'o' ; '.' ; 'm' ; '+' ; '#' ; '#' ; 'd' ; '#' ; 'r' ; '#' ; 'd' ; 'r' ; 'r' ; '.' ; 'f' ; '.' ] ;; (* load scenario1 ;; step () ;; *) (* load scenario2 ;; step () ;; *)