Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / plugins / tiny / tiny_results.ml @ 9b0432bc

History | View | Annotate | Download (1.21 KB)

1
open Tiny
2
open Tiny_utils
3
open Yojson
4

    
5
module Make (Dom : Relational.Domain) = struct
6
  (* Take a mapping of annotations, top value of the domain and a location 
7
    and return a JSON of the form : 
8
    { "time1": "Domain description at time 1", 
9
      "time2": "Domain description at time 2"...}
10
  *)
11
  let dom_values_at_location_to_json m top l =
12
      (* Extracting associated unrolled info *)
13
      let ind = Location.MapInd.filter (fun (l',_) a -> l = l' && not(Dom.order top a)) (snd m) in
14
      let ind = Location.MapInd.bindings ind in
15
      let ind = List.sort (fun (i1, _) (i2, _) -> compare i1 i2) ind in
16
      begin
17
        `Assoc (
18
          List.map (fun ((_,i), e) ->
19
              (string_of_int i), (Dom.json e)
20
        )  ind)
21
      end
22

    
23
  let to_json mapping tiny_encoding  = 
24
    let top = Dom.top (Ast.vars_of_stm tiny_encoding.ast) in
25
    (* giving mapping of annotations and the top value of the domain first *)
26
    let dom_values_at_location_to_json = dom_values_at_location_to_json mapping top  in
27
    (* then give the location where interested in,
28
       to obtain the JSON object with the abstract value at each tick
29
    *)
30
    dom_values_at_location_to_json (Location.beg_p tiny_encoding.location_beg_while)
31
end