package lutin

  1. Overview
  2. Docs
Lutin: modeling stochastic reactive systems

Install

dune-project
 Dependency

Authors

Maintainers

Sources

lutin.2.71.10.tgz
md5=4d07d1263dbc90ab18cbaec55a57dcfe
sha512=2e899aee5e44826827b3626771f7ce01241b1745d48f30b60404cc5cbaa44ac608920e9af3bf171275c429a8b823b3cee7542199b7c4c32919b6bb37e33bf8de

doc/src/lutin/lucky.ml.html

Source file lucky.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
(*-----------------------------------------------------------------------
** Copyright (C) - Verimag.
** This file may only be copied under the terms of the CeCill
** Public License
**-----------------------------------------------------------------------
**
** File: lucky.ml
** Author: erwan.jahier@univ-grenoble-alpes.fr
*)

(****************************************************************************)

open List
open Exp
open Var
open Prog

(****************************************************************************)
(****************************************************************************)

type cs  = Prog.ctrl_state
type csl = cs list
(* type sl  = subst list *)
type sl  = Value.OfIdent.t


(****************************************************************************)
let (draw_values : Var.env_in -> Prog.state -> int -> Thickness.numeric -> 
     FGen.t list -> FGen.t list * csl * (sl * sl) list) =
  fun input state p num_thickness ral ->
    let bool_to_gen_l = state.s.bool_vars_to_gen 
    and num_to_gen_l = state.s.num_vars_to_gen in
    let list_to_formula l =
      if l = [] then True else
	     List.fold_left (fun acc vn -> (And(Bvar(vn), acc)))
	       (Bvar(hd l)) (tl l)
    in
    let bool_to_gen_fl = List.map list_to_formula bool_to_gen_l in
    let rec loop_choose_formula bool_to_gen_f num_to_gen ra =
      let ctx_msg = Prog.ctrl_state_to_string_long state.d.ctrl_state in 
      let vl = state.d.verbose in
      let ra, f, cs = ra.FGen.choose_one_formula () in
      match
	     Solver.solve_formula state.d.snt input state.d.memory vl ctx_msg
        state.s.output_var_names p num_thickness bool_to_gen_f num_to_gen f 
		with
        | _snt, [] ->  (* The constraint is unsatisfiable because of the numerics *)
          loop_choose_formula bool_to_gen_f num_to_gen ra
        | _,sol_l -> ra, f, cs, sol_l
    in
    let (ral, _fl, csl, sol_ll) = 
      Util.list_split4(
        Util.list_map3 loop_choose_formula bool_to_gen_fl num_to_gen_l ral) 
    in
    (* fl is a list of formula that should actually be considered
       as a conjunction.  But because of the thickness, when we
       draw values in each formula in turn, we obtain a list of
       list that ougth to be transposed.  *)
    let sol_ll : (sl * sl) list list =  Util.transpose sol_ll in
    let (merge_sol : (sl * sl) list -> sl * sl) =
      fun sol_l -> (* Merge solutions coming from the fl: in other terms, we
                      interpret the formula list as a conjunction. *)
        List.fold_left
          (fun  (acc1, acc2) (sl1,sl2) -> (Value.OfIdent.union sl1 acc1, Value.OfIdent.union sl2 acc2))
          (Value.OfIdent.empty,Value.OfIdent.empty) 
          sol_l
    in
    let sol_l = List.map merge_sol sol_ll in
    assert (List.length ral = List.length csl);
		(* ZARBI 2010/12/10 *)
      (* assert (List.length ral = List.length sol_l); *)
    ral, csl,  sol_l


(****************************************************************************)
(*****************************************************************************)

(* Returns the subst for a memory box, if it can be computed *)
let (maybe_update_one_pre_var : env_in -> env_out -> env_loc -> sl ->
       Var.name * Exp.var -> subst option) =
  fun input (output:sl) (local:sl) (memory:sl) (pre_vn, vn) ->
    try (
      let v =
	match Var.mode vn with
	  | Input  -> Value.OfIdent.get input (Var.name vn)
	  | Output -> Value.OfIdent.get output (Var.name vn)
	  | Local  -> Value.OfIdent.get local (Var.name vn) 
	  | Pre -> Value.OfIdent.get memory (Var.name vn) 
      in
	Some (pre_vn,v)
    )   
    with Not_found -> None

      (* E.g., at the second step, input vars migth still not
	 be available if the env starts to generate outputs. *)
   
(** [update_pre input output local] Updates the values of pre
    variables (updating [env_state.pre]) with [input], [output], and
    [local].  *)
let (update_pre: env_in -> env_out -> env_loc -> Prog.state -> sl) =
  fun input output local state ->
    let maybe_pre =
      List.map (maybe_update_one_pre_var input output local state.d.memory)
	state.s.memories_names
    in
    let sl =
      (* OBSOLETE
      ( List.fold_left
	  (fun acc ms ->
	     match ms with
	     | Some(s) -> (s::acc)
	     | None -> acc
	  )
	  []
	  maybe_pre
      )
      *)
      ( List.fold_left
	  (fun acc ms ->
	     match ms with
	     | Some(s) -> (Value.OfIdent.add acc s)
	     | None -> acc
	  )
	  Value.OfIdent.empty
	  maybe_pre
      )
    in
      if state.d.verbose >= 3 then (
	print_string "*** Update the memory: \n";
	(* print_subst_list sl stdout; *)
	Value.OfIdent.print sl stdout;
	print_string "\n";
	List.iter (fun (x,_) -> print_string (x^" ")) state.s.memories_names;
	print_string "\n";
	flush stdout
      );
      sl

(*****************************************************************************)
(*****************************************************************************)


type step_mode =  StepInside | StepEdges | StepVertices
type solution =  Var.env_out * Var.env_loc


(* We save the inputs and the outputs in order to be able to restore them easily
   when the automata is blocked (when no transition can be taken in the 
   reactive mode).
*)
let previous_output = ref None
let previous_local = ref None

let (env_try_do : Thickness.formula_draw_nb * Thickness.numeric -> env_in -> 
      Prog.state -> FGen.t list -> (env_out * env_loc) list -> 
       FGen.t list * csl * (env_out * env_loc) list) =
  fun (p, num_thickness) input state ral acc ->
    let  ral', csl', sol = (draw_values input state p num_thickness ral) in
      ral', csl', (rev_append acc sol)
    
(* Exported *)
let (env_try : Thickness.t -> env_in -> Prog.state -> FGen.t list -> 
      FGen.t list * (env_out * env_loc) list) =
  fun (bt,nt) input state ral ->
(*     let ral = LucFGen.get input state in *)
    if fst bt then
      (* try all formula *)
      let rec f ral acc =
	try
	  let ral', _csl, acc' = env_try_do (snd bt,nt) input state ral acc in
	    f ral' acc'
	with 
	    FGen.NoMoreFormula -> ral,acc
      in
	f ral []
    else
      let (ral', _csl, sol) = env_try_do (snd bt,nt) input state ral [] in
	ral', sol
	
(*****************************************************************************)
(* Exported *)
let (env_step : step_mode -> env_in -> Prog.state ref -> FGen.t list -> 
     solution) =
  fun step_mode input state_ref ral ->
    let state = !state_ref in
    let thick =
      match step_mode with
	   | StepInside -> (1, 0, Thickness.AtMost 0)
	   | StepEdges -> (0, 1, Thickness.AtMost 0)
	   | StepVertices -> (0, 0, Thickness.AtMost 1)
    in
    try
      Utils.time_C "env_try_do";
	   let (_ral', csl, soll) = env_try_do (1, thick) input state ral [] in
      Utils.time_R "env_try_do";
	   let (output, local) = assert( soll <> []); List.hd soll in
	   let new_state_dyn = {
	     memory = update_pre input output local state;
	     ctrl_state = csl;
	     last_input = input;
	     last_output = output;
	     last_local  = local;
        snt = Bddd.clear state.d.snt;
	     verbose = state.d.verbose
	   }
	   in	
	   let new_state = { d = new_state_dyn ; s = state.s } in

	   previous_output := Some output;
	   previous_local := Some local;
      state_ref:= new_state;
	   (output, local)
    with
	   FGen.NoMoreFormula  -> 
	   match (!previous_output, !previous_local) with
	   | Some(out), Some(loc) ->
		  if state.s.reactive then 
		    (
		      if state.d.verbose >= 1 then 
			     print_string (
			       "### No transition is available; " ^ 
			       "values of the previous cycle are used.\n");
		      flush stdout;
		      (out, loc)
		    ) 
		  else
		    (
		      if state.d.verbose >= 1 then 
			     print_string (
			       "# No transition is labelled by a satisfiable formula.\n" ^
			       "# The program is blocked.\n");
		      flush stdout;
		      raise FGen.NoMoreFormula
		    )
	   | _, _ -> raise FGen.NoMoreFormula

OCaml

Innovation. Community. Security.