package electrod
Formal analysis for the Electrod formal pivot language
Install
Dune Dependency
Authors
Maintainers
Sources
electrod-1.0.0.tbz
sha256=4da251e58d97c797d6e940e586d225a09715777fbb1b25c5527a6a2e1e3c2d58
sha512=89c45ebd0d3401b17eac4217289ed21ec87135ab5fa62bf63b2bed1ad1435a381e3434582c2ec99c2e6d8d87ce23cecfa7ba14d76234493992ae06879b808dd2
doc/src/electrod.libelectrod/Exp_bounds.ml.html
Source file Exp_bounds.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 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368
(******************************************************************************* * 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 ******************************************************************************) open Containers module G = Elo module TS = Tuple_set type bounds = { must : TS.t ; sup : TS.t ; may : TS.t } let pp_subst out subst = Fmtc.(brackets @@ list @@ parens @@ pair ~sep:comma int Tuple.pp) out (List.mapi (fun i tuple -> (i, tuple)) subst) (* says whether all tuples in a list are different from one another *) let rec alldiff (tuples : Tuple.t list) : bool = match tuples with | [] -> true | hd :: tl when List.mem ~eq:Tuple.equal hd tl -> false | _ :: tl -> alldiff tl (* [sets] is a list of tuple sets, but a tuple set is expected to be given as a list of tuples. Returns a list of tuple lists: each of these represents a single tuple in the cartesian product, but not concatenated into a single long tuple yet (because these tuples will have to be composed with others before creating a really-long tuple) E.g.: suppose `set = [(1, 2); (3, 4)]`. Then we obtain, for `n = 3`: [ [(3, 4); (3, 4); (3, 4)]; [(3, 4); (3, 4); (1, 2)]; [(3, 4); (1, 2); (3, 4)]; [(3, 4); (1, 2); (1, 2)]; [(1, 2); (3, 4); (3, 4)]; [(1, 2); (3, 4); (1, 2)]; [(1, 2); (1, 2); (3, 4)]; [(1, 2); (1, 2); (1, 2)] ] *) let nproduct (n : int) (disj : bool) (set : Tuple.t list) : Tuple.t list list = List.repeat n [ set ] (* returns (a list of) lists of tuples: *) |> List.cartesian_product (* possibly remove such lists that contain several instance of the same tuple *) |> if disj then List.filter alldiff else Fun.id (* The must of a compr set is empty. Indeed, it would be wrong to compute the must from the sim_bindings only, because the formula could be in contradiction with this must. Taking the formula into account is not possible, so we consider an empty must. *) let sup_sim_binding fbounds_exp (subst : Tuple.t list) (disj, nbvars, range) : Tuple.t list list = (* compute the bound for the range of *this* sim binding. NOTE: [range] is given as a [Tuple.t list] instead of a [TS.t] for technical purposes only. As a consequence, the returned value for the whole function is a set of sets of tuples represented by a list of lists... *) let { sup; _ } = fbounds_exp (range, subst) in let sup_as_list = TS.to_list sup in (* compute the exponent for this bindings (NOTE: tuples are not concatenated, just put in the same list representing a combination of tuples). E.g.: suppose `range = [(1, 2); (3, 4)]`. Then we obtain, for `nbvars = 3`: [ [(3, 4); (3, 4); (3, 4)]; [(3, 4); (3, 4); (1, 2)]; [(3, 4); (1, 2); (3, 4)]; [(3, 4); (1, 2); (1, 2)]; [(1, 2); (3, 4); (3, 4)]; [(1, 2); (3, 4); (1, 2)]; [(1, 2); (1, 2); (3, 4)]; [(1, 2); (1, 2); (1, 2)] ] *) nproduct nbvars disj sup_as_list (* Computes the bounds for sim_bindings, in the case of a set defined by comprehension. The whole idea of this function (and the following auxiliary ones) is to apply the following scheme. Say we want to compute: sup({x : s, y : x.r | ...}) The result must be: sup(s) -> { UNION_(tuple in sup(s)) sup( x.r [tuple/x] ) } as every pair in the comprehension is s.t. the range for y depends on the value for x. E.g.: Taking sup(s) = { a b }, sup(r) = { (a b) (b c) (a c) (a d) }: x : s, y : x.r should yield: (a x a.r) union (b x b.r) = {(a b) (a c) (a d) (b c)} So what we do is the following: Walk left-to-right along some sim_bindings and compute the corresponding bound, while accumulating already computed bounds. Finally everything is composed. [subst] is a substitution from already-visited sim_bindings. [fbound] is the function returning the bound. *) let rec sup_sim_bindings fbounds_exp (subst : Tuple.t list) sim_bindings : Tuple.t list = Msg.debug (fun m -> m "IN sup_sim_bindings %a %a" pp_subst subst G.(pp_sim_bindings (List.length subst)) sim_bindings); ( match sim_bindings with | [] -> assert false | [ sim_binding ] -> (* compute the product of bounds for the head sim_binding *) sup_sim_binding fbounds_exp subst sim_binding (* base case => convert back into a list of tuples *) |> List.map Tuple.concat | hd :: tl -> let hd_sup = sup_sim_binding fbounds_exp subst hd in (* as explained above in the example: for every possible combination of tuples in [hd_sup], we have to substitute *this* combination in the tail, then compute the resulting product and add it to the whole possibilities *) List.fold_left (fun acc line -> acc @ product_for_one_hd_combination fbounds_exp subst tl line) [] hd_sup ) |> Fun.tap (fun res -> Msg.debug (fun m -> m "OUT sup_sim_bindings %a %a = %a" pp_subst subst G.(pp_sim_bindings (List.length subst)) sim_bindings Fmtc.(braces @@ list ~sep:sp @@ Tuple.pp) res)) (* given the list of tuples corresponding to the bound for the head sim binding (so it's a list of tuples, as there are multiple variables bound to a given range), compute all the products with all the results obtained by substituting in the tail according to the substitutions induced by the said head tuples. [fbounds_exp] is the function computing the bound (it is cached below in the file) *) and product_for_one_hd_combination fbounds_exp subst (tl : (bool * int * G.exp) list) (hd_combination : Tuple.t list) = let tl_sup = sup_sim_bindings fbounds_exp (List.rev hd_combination @ subst) tl in List.product Tuple.( @@@ ) [ Tuple.concat hd_combination ] tl_sup (* In all the following functions, [subst] is a *stack* ot tuples, meaning tuples (corresponding to DB indices) appear reversed wrt their order of binding. Then index 0 refers to the last (nearest) binding. *) let make_bounds_exp = let return_bounds (exp, subst) must sup = if not (TS.subset must sup) then Msg.err (fun m -> m "%s.bounds@ %a@ with@\n\ subst= %a@\n\ @\n\ must(%a)=@ %a@\n\ sup(%a)=@ %a@." __MODULE__ (G.pp_exp @@ List.length subst) exp pp_subst subst (G.pp_exp @@ List.length subst) exp TS.pp must (G.pp_exp @@ List.length subst) exp TS.pp sup); { must; sup; may = TS.diff sup must } in let eq x1 x2 = CCEqual.(pair physical (list Tuple.equal)) x1 x2 in let hash x = Hash.(pair (fun (G.Exp { hkey; _ }) -> hkey) (list Tuple.hash)) x in (* let cb ~in_cache (e, subst) __value = Fmtc.(pr "@[<h>Cache search for %a: %B@]@\n" (pair ~sep:sp (brackets @@ list ~sep:comma Tuple.pp) (G.pp_exp (List.length subst))) (subst, e) in_cache) in *) let cache = CCCache.unbounded ~eq ~hash 1793 in fun domain -> CCCache.with_cache_rec cache (fun fbounds_exp ((G.Exp { node = { prim_exp = pe; _ }; _ }, subst) as args) -> let open G in match pe with | Var v -> ( match List.get_at_idx v subst with | None -> Fmt.kstrf failwith "%s.bounds_prim_exp: no variable %d in substitution %a" __MODULE__ v pp_subst subst | Some tuple -> let singleton = TS.singleton tuple in return_bounds args singleton singleton ) | Name n -> let rel = Domain.get_exn n domain in return_bounds args (Relation.must rel) (Relation.sup rel) | None_ -> return_bounds args TS.empty TS.empty | Univ -> let univ = Domain.univ_atoms domain in return_bounds args univ univ | Iden -> let iden = Domain.get_exn Name.iden domain in return_bounds args (Relation.must iden) (Relation.sup iden) | RUn (Transpose, e) -> let b = fbounds_exp (e, subst) in return_bounds args (TS.transpose b.must) (TS.transpose b.sup) | RUn (TClos, e) -> let b = fbounds_exp (e, subst) in return_bounds args (TS.transitive_closure b.must) (TS.transitive_closure b.sup) |> Fun.tap (fun res -> Msg.debug (fun m -> m "bounds_prim_exp(TClos):@\n\ must(%a) = %a@\n\ may(%a) = %a" (G.pp_prim_exp @@ List.length subst) pe TS.pp res.must (G.pp_prim_exp @@ List.length subst) pe TS.pp res.may)) | RUn (RTClos, e) -> let iden = Domain.get_exn Name.iden domain in let b = fbounds_exp (e, subst) in return_bounds args (TS.union (TS.transitive_closure b.must) @@ Relation.must iden) (TS.union (TS.transitive_closure b.sup) @@ Relation.sup iden) |> Fun.tap (fun res -> Msg.debug (fun m -> m "bounds_prim_exp(TClos):@\n\ must(%a) = %a@\n\ may(%a) = %a" (G.pp_prim_exp @@ List.length subst) pe TS.pp res.must (G.pp_prim_exp @@ List.length subst) pe TS.pp res.may)) | RBin (e1, Union, e2) -> let b1 = fbounds_exp (e1, subst) in let b2 = fbounds_exp (e2, subst) in return_bounds args (TS.union b1.must b2.must) (TS.union b1.sup b2.sup) | RBin (e1, Inter, e2) -> let b1 = fbounds_exp (e1, subst) in let b2 = fbounds_exp (e2, subst) in return_bounds args (TS.inter b1.must b2.must) (TS.inter b1.sup b2.sup) | RBin (e1, Over, e2) -> let b1 = fbounds_exp (e1, subst) in let b2 = fbounds_exp (e2, subst) in return_bounds args (TS.override b1.must b2.must) (TS.override b1.sup b2.sup) | RBin (e1, LProj, e2) -> let b1 = fbounds_exp (e1, subst) in let b2 = fbounds_exp (e2, subst) in return_bounds args (TS.lproj b1.must b2.must) (TS.lproj b1.sup b2.sup) | RBin (e1, RProj, e2) -> let b1 = fbounds_exp (e1, subst) in let b2 = fbounds_exp (e2, subst) in return_bounds args (TS.rproj b1.must b2.must) (TS.rproj b1.sup b2.sup) | RBin (e1, Prod, e2) -> let b1 = fbounds_exp (e1, subst) in let b2 = fbounds_exp (e2, subst) in return_bounds args (TS.product b1.must b2.must) (TS.product b1.sup b2.sup) | RBin (e1, Diff, e2) -> let b1 = fbounds_exp (e1, subst) in let b2 = fbounds_exp (e2, subst) in (* compute the tuples that are necessarily in e1 and necessarily not in e2 *) let must_diff = TS.filter (fun tup -> not (TS.mem tup b2.sup)) b1.must in return_bounds args must_diff (TS.diff b1.sup b2.must) (* b2.MUST! *) | RBin (e1, Join, e2) -> let b1 = fbounds_exp (e1, subst) in let b2 = fbounds_exp (e2, subst) in return_bounds args (TS.join b1.must b2.must) (TS.join b1.sup b2.sup) | RIte (_, e1, e2) -> let b1 = fbounds_exp (e1, subst) in let b2 = fbounds_exp (e2, subst) in return_bounds args (TS.inter b1.must b2.must) (TS.union b1.sup b2.sup) | Prime e -> fbounds_exp (e, subst) | Compr (sim_bindings, _) -> let sup_list = sup_sim_bindings fbounds_exp subst sim_bindings in return_bounds args TS.empty (TS.of_tuples sup_list))
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>