Source file `Elo_to_smv1.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
(*******************************************************************************
 * electrod - a model finder for relational first-order linear temporal logic
 * 
 * Copyright (C) 2016-2020 ONERA
 * Authors: Julien Brunel (ONERA), David Chemouil (ONERA)
 * 
 * This Source Code Form is subject to the terms of the Mozilla Public
 * License, v. 2.0. If a copy of the MPL was not distributed with this
 * file, You can obtain one at http://mozilla.org/MPL/2.0/.
 * 
 * SPDX-License-Identifier: MPL-2.0
 * License-Filename: LICENSE.md
 ******************************************************************************)

(** Provides a transformation from Electrod models to SMV models. Uses
   enumerations when possible. *)

open Containers

module SMV_atom : Solver.ATOMIC_PROPOSITION = struct
  type t =
    { sym : Symbol.t
    ; (* hashconsed strings *)
      const : bool
    ; partial : bool
    ; (* is 'lone'? *)
      dom_arity : int option
          (* arity of the domain (>=0) if functional, else None *)
    }

  let compare { sym = sym1; _ } { sym = sym2; _ } = Symbol.compare sym1 sym2

  let compare_string { sym = sym1; _ } { sym = sym2; _ } =
    Symbol.compare_string sym1 sym2


  let pp fmt at = Symbol.pp fmt at.sym

  let equal { sym = sym1; _ } { sym = sym2; _ } = Symbol.equal sym1 sym2

  let hash at = Symbol.hash at.sym

  let domain_arity t = t.dom_arity

  let is_const t = t.const

  let is_partial t = t.partial

  (* table tracking which pair (name, tuple) a string comes from. Uses
     hahsconsing to make this more efficient *)
  module HT = CCHashtbl.Make (Symbol)

  let names_and_tuples = HT.create 179

  (* usually less than that many VARs *)

  let rel_sep = "-"

  let atom_sep = Fmtc.minus

  let make domain name tuple =
    let rel = Domain.get_exn name domain in
    let dom_arity =
      let open Scope in
      match Relation.scope rel with
      | Exact _ ->
          assert false
      | Inexact (Plain_relation _) ->
          None
      | Inexact (Partial_function (ar, _)) ->
          Some ar
      | Inexact (Total_function (ar, _)) ->
          Some ar
    in
    let const = Relation.is_const rel in
    let partial = rel |> Relation.scope |> Scope.is_partial in
    let ats = Tuple.to_list tuple in
    let name_str =
      let s = Fmtc.to_to_string Name.pp name in
      if String.prefix ~pre:"$" s
      then (* Skolem vars may have a name incompatible with SMV so: *)
        "_" ^ s
      else s
    in
    let full_str =
      Format.sprintf
        "%s%s%a"
        name_str
        rel_sep
        Fmtc.(list ~sep:atom_sep Atom.pp)
        ats
    in
    let sym = Symbol.make full_str in
    (* keep track of creations to allow to get original pairs back *)
    HT.add names_and_tuples sym (name, tuple);
    { sym; dom_arity; const; partial }


  let split at = HT.get names_and_tuples at.sym

  let split_string str = HT.get names_and_tuples (Symbol.make str)
end

module SMV_LTL = Smv.Make_SMV_LTL (SMV_atom)
module SMV_file_format = Smv.Make_SMV_file_format (SMV_LTL)
module Elo_to_SMV_LTL = Elo_to_ltl1.Make (SMV_LTL)
module Elo_to_SMV_model =
  Elo_to_model1.Make (SMV_LTL) (Elo_to_SMV_LTL) (SMV_file_format)

let pp = SMV_file_format.pp

let analyze = SMV_file_format.analyze

(* temporary *)
let run (elo, temporal_symmetry, symmetry_offset) =
  Elo_to_SMV_model.run (elo, temporal_symmetry, symmetry_offset)


let transfo = Transfo.make "to_smv1" run