-
Notifications
You must be signed in to change notification settings - Fork 1
Expand file tree
/
Copy pathalgorithm.mli
More file actions
72 lines (62 loc) · 2.85 KB
/
Copy pathalgorithm.mli
File metadata and controls
72 lines (62 loc) · 2.85 KB
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
(*
* This file is part of MONPOLY.
*
* Copyright (C) 2011 Nokia Corporation and/or its subsidiary(-ies).
* Contact: Nokia Corporation (Debmalya Biswas: [email protected])
*
* Copyright (C) 2012 ETH Zurich.
* Contact: ETH Zurich (Eugen Zalinescu: [email protected])
*
*
* This library is free software; you can redistribute it and/or
* modify it under the terms of the GNU Lesser General Public License
* as published by the Free Software Foundation, version 2.1 of the
* License.
*
* This library is distributed in the hope that it will be useful, but
* WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
* Lesser General Public License for more details.
*
* You should have received a copy of the GNU Lesser General Public
* License along with this library. If not, see
* http://www.gnu.org/licenses/lgpl-2.1.html.
*
* As a special exception to the GNU Lesser General Public License,
* you may link, statically or dynamically, a "work that uses the
* Library" with a publicly distributed version of the Library to
* produce an executable file containing portions of the Library, and
* distribute that executable file under terms of your choice, without
* any of the additional requirements listed in clause 6 of the GNU
* Lesser General Public License. By "a publicly distributed version
* of the Library", we mean either the unmodified Library as
* distributed by Nokia, or a modified version of the Library that is
* distributed under the conditions defined in clause 3 of the GNU
* Lesser General Public License. This exception does not however
* invalidate any other reasons why the executable file might be
* covered by the GNU Lesser General Public License.
*)
(** This module implements the monitoring algorithm. *)
open Predicate
open MFOTL
val combine_files: string ref
val resumefile: string ref
val dumpfile: string ref
(** The names of the files used for state saving and state loading. *)
val resume: string -> unit
val combine: string -> unit
(* val resume: string -> unit *)
(** [resume log] loads the monitor state from file [resumefile] and
then monitors the log [log]. *)
val monitor_string: string -> var list -> formula -> unit
(** [monitor log fv f] monitors the log string [log] with regard to the
formula [f]. For each time point, it outputs, as soon as possible,
the tuples satisfying formula [f]. The tuples are sorted according to
the variable list [fv]. *)
val monitor: string -> var list -> formula -> unit
(** [monitor log f] monitors the log [log] with regard to the
formula [f]. For each time point, it outputs, as soon as possible,
the tuples satisfying formula [f]. The tuples are sorted according to
the variable list [fv]. *)
val test_filter: string -> formula -> unit
val run_test: string -> formula -> unit