-
Notifications
You must be signed in to change notification settings - Fork 1
Expand file tree
/
Copy pathalgorithm.ml
More file actions
1965 lines (1754 loc) · 63 KB
/
Copy pathalgorithm.ml
File metadata and controls
1965 lines (1754 loc) · 63 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
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
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(*
* 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. This algorithm is
described in the paper "Runtime Monitoring of Metric First-order
Temporal Properties" by David Basin, Felix Klaedtke, Samuel
Muller, and Birgit Pfitzmann, presented at FSTTCS'08.
This is the MONPOLY's main module, all other modules can be seen
as "helper" modules. The module's entry point is normally the
[monitor] function. This function checks that the given formula is
monitorable and then calls the [check_log] function which
iteratively reads each log entry. To be able to incrementally
process the entries, the input formula is first extended with
additional information for each subformula, by calling the
[add_ext] function. Also, a queue [neval] of not-yet evaluated
indexes of log entries is maintained.
The function [check_log] reads each log entry, calls [add_index]
to update the extended formula with the new information from the
entry at index [i], adds index [i] to the queue of not-yet
evaluated indexes, and finally calls [process_index] to process
this entry.
The function [process_index] iterativelly tries to evaluate the
formula at each index (calling the function [eval]) from the queue
of not-yet evaluated indexes. It stops when the formula cannot be
evaluated or when the formula has been evaluated at all indexes in
the queue. The function [eval] performs a bottom-up evaluation of
the formula.
*)
open Dllist
open Misc
open Perf
open Predicate
open MFOTL
open Tuple
open Relation
open Table
open Db
open Log
open Sliding
open Helper
open Marshalling
open Splitting
open Extformula
open Mformula
open Hypercube_slicer
module Sk = Dllist
module Sj = Dllist
let resumefile = ref ""
let dumpfile = ref ""
let combine_files = ref ""
let lastts = ref MFOTL.ts_invalid
let slicer_heavy_unproc : (int * string list) array ref= ref [|(0, [])|]
let slicer_shares = ref [|[||]|]
let slicer_seeds = ref [|[||]|]
(* For the sake of clarity, think about merging these types and all
related functions. Some fields will be redundant, but we will not lose
that much. *)
let crt_ts = ref MFOTL.ts_invalid
let crt_tp = ref (-1)
let make_db db =
Db.make_db (List.map (fun (s,r) -> Table.make_table s r) db)
let mqueue_add_last auxrels tsq rel2 =
if Mqueue.is_empty auxrels then
Mqueue.add (tsq,rel2) auxrels
else
let tslast, rellast = Mqueue.get_last auxrels in
if tslast = tsq then
Mqueue.update_last (tsq, Relation.union rellast rel2) auxrels
else
Mqueue.add (tsq,rel2) auxrels
let dllist_add_last auxrels tsq rel2 =
if Dllist.is_empty auxrels then
Dllist.add_last (tsq,rel2) auxrels
else
let tslast, rellast = Dllist.get_last auxrels in
if tslast = tsq then
let _ = Dllist.pop_last auxrels in
Dllist.add_last (tsq, Relation.union rellast rel2) auxrels
else
Dllist.add_last (tsq,rel2) auxrels
(* [saauxrels] consists of those relations that are outside of the
relevant time window *)
let update_since_all intv tsq inf comp rel1 rel2 =
inf.sres <- comp inf.sres rel1;
let auxrels = inf.saauxrels in
let rec elim () =
if not (Mqueue.is_empty auxrels) then
let (tsj,relj) = Mqueue.top auxrels in
if MFOTL.in_right_ext (MFOTL.ts_minus tsq tsj) intv then
begin
ignore (Mqueue.pop auxrels);
inf.sres <- Relation.union inf.sres (comp relj rel1);
elim ()
end
in
elim ();
Mqueue.update_and_delete
(fun (tsj, relj) -> (tsj, comp relj rel1))
(fun (_,relj) -> Relation.is_empty relj) (* delete the current node if newrel is empty *)
auxrels;
if not (Relation.is_empty rel2) then
begin
if MFOTL.in_right_ext MFOTL.ts_null intv then
inf.sres <- Relation.union inf.sres rel2;
mqueue_add_last auxrels tsq rel2
end;
inf.sres
let update_since intv tsq auxrels comp discard rel1 rel2 =
let rec elim_old_auxrels () =
(* remove old elements that felt out of the interval *)
if not (Mqueue.is_empty auxrels) then
let (tsj,relj) = Mqueue.top auxrels in
if not (MFOTL.in_left_ext (MFOTL.ts_minus tsq tsj) intv) then
begin
ignore(Mqueue.pop auxrels);
elim_old_auxrels()
end
in
elim_old_auxrels ();
let res = ref Relation.empty in
Mqueue.update_and_delete
(fun (tsj,relj) ->
let newrel = comp relj rel1 in
if (not discard) && MFOTL.in_right_ext (MFOTL.ts_minus tsq tsj) intv then
res := Relation.union !res newrel;
(tsj,newrel)
)
(* delete the current node if newrel is empty *)
(fun (_,relj) -> Relation.is_empty relj)
auxrels;
if not (Relation.is_empty rel2) then
begin
if (not discard) && MFOTL.in_right_ext MFOTL.ts_null intv then
res := Relation.union !res rel2;
mqueue_add_last auxrels tsq rel2
end;
!res
let update_once_all intv tsq inf =
let auxrels = inf.oaauxrels in
let rec comp () =
if not (Mqueue.is_empty auxrels) then
let (tsj,relj) = Mqueue.top auxrels in
if MFOTL.in_right_ext (MFOTL.ts_minus tsq tsj) intv then
begin
ignore (Mqueue.pop auxrels);
inf.ores <- Relation.union inf.ores relj;
comp ()
end
in
comp ()
(* Remark: we could remove all auxrels that are covered by the tree and
gain some memory (sooner). However detecting [lw] would be harder. *)
let update_once_zero intv q tsq inf rel2 discard =
let auxrels = inf.ozauxrels in
let rec elim_old_ozauxrels () =
(* remove old elements that fell out of the interval *)
if not (Dllist.is_empty auxrels) then
let (_, tsj, arel) = Dllist.get_first auxrels in
if not (MFOTL.in_left_ext (MFOTL.ts_minus tsq tsj) intv) then
begin
if inf.ozlast != Dllist.void && inf.ozlast == Dllist.get_first_cell auxrels then
inf.ozlast <- Dllist.void;
ignore(Dllist.pop_first auxrels);
elim_old_ozauxrels()
end
in
elim_old_ozauxrels ();
if not (Relation.is_empty rel2) then
Dllist.add_last (q,tsq,rel2) inf.ozauxrels;
if Dllist.is_empty auxrels || discard then
Relation.empty
else
let cond = fun _ -> true in
let f = fun (j,_,rel) -> (j,rel) in
let subseq, new_last = get_new_elements auxrels inf.ozlast cond f in
let lw,_,_ = Dllist.get_first auxrels in
let rw =
if subseq = [] then
let j,_,_ = Dllist.get_data inf.ozlast in j
else
begin
assert (new_last != Dllist.void);
inf.ozlast <- new_last;
let rw = fst (List.hd subseq) in
assert (rw = let j,_,_ = Dllist.get_data new_last in j);
rw
end
in
if Misc.debugging Dbg_eval then
begin
Printf.printf "[update_once_zero] lw = %d rw = %d " lw rw;
Misc.printnl_list "subseq = " print_auxel subseq;
end;
let newt = Sliding.slide string_of_int Relation.union subseq (lw, rw) inf.oztree in
inf.oztree <- newt;
Sliding.stree_res newt
let update_once intv tsq inf discard =
let auxrels = inf.oauxrels in
let rec elim_old_oauxrels () =
(* remove old elements that fell out of the interval *)
if not (Dllist.is_empty auxrels) then
let (tsj,_) = Dllist.get_first auxrels in
if not (MFOTL.in_left_ext (MFOTL.ts_minus tsq tsj) intv) then
begin
if inf.olast != Dllist.void && inf.olast == Dllist.get_first_cell auxrels then
inf.olast <- Dllist.void;
ignore(Dllist.pop_first auxrels);
elim_old_oauxrels()
end
in
elim_old_oauxrels ();
(* In the following we distiguish between the new window and the new
elements: the new window may contain old elements (the old and new
windows may overlap). *)
if Dllist.is_empty auxrels || discard then
Relation.empty
else
let lw = fst (Dllist.get_first auxrels) in
if MFOTL.in_right_ext (MFOTL.ts_minus tsq lw) intv then
(* the new window is not empty *)
let cond = fun (tsj,_) -> MFOTL.in_right_ext (MFOTL.ts_minus tsq tsj) intv in
let subseq, new_last = get_new_elements auxrels inf.olast cond (fun x -> x) in
let rw =
if subseq = [] then
fst (Dllist.get_data inf.olast)
else
begin
assert (new_last != Dllist.void);
inf.olast <- new_last;
let rw = fst (List.hd subseq) in
assert (rw = fst (Dllist.get_data new_last));
rw
end
in
if Misc.debugging Dbg_eval then
begin
Printf.printf "[update_once] lw = %s rw = %s "
(MFOTL.string_of_ts lw)
(MFOTL.string_of_ts rw);
Misc.printnl_list "subseq = " print_sauxel subseq;
end;
let newt = Sliding.slide MFOTL.string_of_ts Relation.union subseq (lw, rw) inf.otree in
inf.otree <- newt;
Sliding.stree_res newt
else
begin
(* the new window is empty,
because not even the oldest element satisfies the constraint *)
inf.otree <- LNode {l = MFOTL.ts_invalid;
r = MFOTL.ts_invalid;
res = Some (Relation.empty)};
inf.olast <- Dllist.void;
Relation.empty
end
let update_old_until q tsq i intv inf discard =
(* eliminate those entries (q-1,reli) from rels;
return the tuples which hold at q *)
let elim_old j rels =
assert(j>=q-1);
if not (Sk.is_empty rels) then
let (k,relk) = Sk.get_first rels in
if k=q-1 then
begin
ignore(Sk.pop_first rels);
if not (Sk.is_empty rels) then
let (k',relk') = Sk.pop_first rels in
assert(k'>=q && j>=q);
let newrelk' = Relation.union relk relk' in
Sk.add_first (k',newrelk') rels;
if k'=q then
newrelk'
else
relk
else
if (j>q-1) then
begin
Sk.add_first (k+1,relk) rels;
relk
end
else
Relation.empty
end
else
begin
assert(k>q-1);
if k=q then
relk
else
Relation.empty
end
else (* Sk.is_empty rels = true *)
Relation.empty
in
let rec elim_old_raux () =
(* remove old elements that fell out of the interval *)
if not (Sj.is_empty inf.raux) then
let (j,tsj,_) = Sj.get_first inf.raux in
if j<q || not (MFOTL.in_right_ext (MFOTL.ts_minus tsj tsq) intv) then
begin
ignore(Sj.pop_first inf.raux);
elim_old_raux()
end
in
elim_old_raux ();
Sj.iter (
fun (j,tsj,rrels) ->
assert(j>=q);
assert(MFOTL.in_right_ext (MFOTL.ts_minus tsj tsq) intv);
let relq = elim_old j rrels in
if (not discard) && not (Relation.is_empty relq) then
inf.ures <- Relation.union inf.ures relq;
if Misc.debugging Dbg_eval then
Relation.print_reln "[update_aux] res: " inf.ures;
) inf.raux;
(* saux holds elements (k,relk) for the last seen index,
i.e. [i] *)
assert(i>=q-1);
if i=q-1 then
Sk.clear inf.saux
else
ignore(elim_old i inf.saux)
(* Auxiliary functions for the f1 Until_I f2 case.
The saux list contains tuples (k,Sk) (ordered incrementally by k),
with q <= k <= i, such that the tuples in Sk satisfy f1
continuously between k and i, and k is minimal (that is, if a tuple
is in Sk it will not also be in Sk' with k'>k.)
The raux list contains tuples (j,tj,Lj) (ordered incrementaly by
j), with q <= j <= i, where Lj is a list of tuples (k,Rk) (ordered
incrementaly by k), with q <= k <= j, such that the tuples in Rk
satisfy f2 at j and satisfy f1 continuously between k and j-1, and
k is minimal (that is, if a tuple is in Rk it will not also be in
Rk' with j>=k'>k.)
NOTE: The iteration through raux to eliminate those tuples <k,Sk>
with k<q (ie. k=q-1) seems unnecessary. If a tuple in Sk satisfies
f1 continuously from k to j, then it also satisfies f1 continuously
from q to j.
*)
let combine2 comp j rels rel2 =
let nrels = Sk.empty() in
let curr_rel2 = ref rel2 in
Sk.iter
(fun (k,rel) ->
let nrel = comp !curr_rel2 rel in
if not (Relation.is_empty nrel) then
Sk.add_last (k,nrel) nrels;
curr_rel2 := Relation.diff !curr_rel2 nrel;
) rels;
if not (Relation.is_empty !curr_rel2) then
Sk.add_last (j,!curr_rel2) nrels;
nrels
let get_relq q rels =
if not (Sj.is_empty rels) then
let (k,relk) = Sj.get_first rels in
if k = q then Some relk
else None
else
None
let update_until q tsq i tsi intv rel1 rel2 inf comp discard =
if Misc.debugging Dbg_eval then
print_uinf "[update_until] inf: " inf;
assert(i >= q);
let nsaux = combine2 Relation.inter i inf.saux rel1 in
if (MFOTL.in_right_ext (MFOTL.ts_minus tsi tsq) intv) &&
not (Relation.is_empty rel2) then
begin
let rrels = combine2 comp i inf.saux rel2 in
Sj.add_last (i,tsi,rrels) inf.raux;
if not discard then
match get_relq q rrels with
| Some rel -> inf.ures <- Relation.union inf.ures rel
| None -> ()
end;
inf.saux <- nsaux
let elim_old_eventually q tsq intv inf =
let auxrels = inf.eauxrels in
let rec elim_old_eauxrels () =
(* remove old elements that fell out of the interval *)
if not (Dllist.is_empty auxrels) then
let (tsj, _) = Dllist.get_first auxrels in
if not (MFOTL.in_right_ext (MFOTL.ts_minus tsj tsq) intv) then
begin
if inf.elast != Dllist.void && inf.elast == Dllist.get_first_cell auxrels then
inf.elast <- Dllist.void;
ignore(Dllist.pop_first auxrels);
elim_old_eauxrels()
end
in
elim_old_eauxrels ()
let warn_if_empty_aggreg {op; default} {Aggreg.empty_rel; Aggreg.rel} =
if empty_rel then
(match op with
| Avg | Med | Min | Max ->
let op_str = MFOTL.string_of_agg_op op in
let default_str = string_of_cst true default in
let msg = Printf.sprintf "WARNING: %s applied on empty relation! \
Resulting value is %s, by (our) convention.\n"
op_str default_str
in
prerr_string msg
| Cnt | Sum -> ());
rel
let add_let_index f n rels =
let rec update = function
| EPred (p, comp, inf) ->
if Predicate.get_name p = n then
List.iter (fun (i,tsi,rel) -> Queue.add (i,tsi, comp rel) inf) rels
else ()
| ELet (p, comp, f1, f2, inf) ->
update f1;
if Predicate.get_name p = n then () else update f2
| ERel _ -> ()
| ENeg f1
| EExists (_,f1)
| EAggOnce (_,_,f1)
| EAggreg (_,_,f1)
| ENext (_,f1,_)
| EPrev (_,f1,_)
| EOnceA (_,f1,_)
| EOnceZ (_,f1,_)
| EOnce (_,f1,_)
| EEventuallyZ (_,f1,_)
| EEventually (_,f1,_) ->
update f1
| EAnd (_,f1,f2,_)
| EOr (_,f1,f2,_)
| ESinceA (_,_,f1,f2,_)
| ESince (_,_,f1,f2,_)
| ENUntil (_,_,f1,f2,_)
| EUntil (_,_,f1,f2,_) ->
update f1;
update f2
in
update f
(* Arguments:
- [f] the current formula
- [crt] the current evaluation point (an neval cell)
- [discard] a boolean; if true then the result is not used
(only a minimal amount of computation should be done);
it should not be propagated for temporal subformulas
(pitfall: possible source of bugs)
*)
let rec eval f crt discard =
let (q,tsq) = Neval.get_data crt in
if Misc.debugging Dbg_eval then
begin
print_extf "\n[eval] evaluating formula\n" f;
Printf.printf "at (%d,%s) with discard=%b\n%!"
q (MFOTL.string_of_ts tsq) discard
end;
match f with
| ERel rel -> Some rel
| EPred (p,_,inf) ->
if Misc.debugging Dbg_eval then
begin
print_string "[eval,Pred] ";
Predicate.print_predicate p;
print_predinf ": " inf
end;
if Queue.is_empty inf
then None
else begin
let (cq,ctsq,rel) = Queue.pop inf in
assert (cq = q && ctsq = tsq);
Some rel
end
| ELet (p, comp, f1, f2, inf) ->
let rec eval_f1 rels =
if Neval.is_last inf.llast then
rels
else
let crt1 = Neval.get_next inf.llast in
match eval f1 crt1 false with
| Some rel ->
inf.llast <- crt1;
let (i, tsi) = Neval.get_data crt1 in
eval_f1 ((i, tsi, comp rel) :: rels)
| None -> rels
in
add_let_index f2 (Predicate.get_name p) (List.rev (eval_f1 []));
eval f2 crt discard
| ENeg f1 ->
(match eval f1 crt discard with
| Some rel ->
let res =
if Relation.is_empty rel then (* false? *)
Relation.singleton (Tuple.make_tuple [])
else
Relation.empty (* true *)
in
Some res
| None -> None
)
| EExists (comp,f1) ->
(match eval f1 crt discard with
| Some rel -> Some (comp rel)
| None -> None
)
| EAnd (comp,f1,f2,inf) ->
(* we have to store rel1, if f2 cannot be evaluated *)
let eval_and rel1 =
if Relation.is_empty rel1 then
(match eval f2 crt true with
| Some _ ->
inf.arel <- None;
Some rel1
| None ->
inf.arel <- Some rel1;
None
)
else
(match eval f2 crt discard with
| Some rel2 ->
inf.arel <- None;
Some (comp rel1 rel2)
| None ->
inf.arel <- Some rel1;
None
)
in
(match inf.arel with
| Some rel1 -> eval_and rel1
| None ->
(match eval f1 crt discard with
| Some rel1 -> eval_and rel1
| None -> None
)
)
| EAggreg (inf, comp, f) ->
(match eval f crt discard with
| Some rel ->
Some (if discard then Relation.empty
else warn_if_empty_aggreg inf (comp rel))
| None -> None
)
| EOr (comp, f1, f2, inf) ->
(* we have to store rel1, if f2 cannot be evaluated *)
(match inf.arel with
| Some rel1 ->
(match eval f2 crt discard with
| Some rel2 ->
inf.arel <- None;
Some (comp rel1 rel2)
| None -> None
)
| None ->
(match eval f1 crt discard with
| Some rel1 ->
(match eval f2 crt discard with
| Some rel2 -> Some (comp rel1 rel2)
| None ->
inf.arel <- Some rel1;
None
)
| None -> None
)
)
| EPrev (intv,f1,inf) ->
if Misc.debugging Dbg_eval then
Printf.printf "[eval,Prev] inf.plast=%s\n%!" (Neval.string_of_cell inf.plast);
if q = 0 then
Some Relation.empty
else
begin
let pcrt = Neval.get_next inf.plast in
let pq, ptsq = Neval.get_data pcrt in
assert(pq = q-1);
match eval f1 pcrt discard with
| Some rel1 ->
inf.plast <- pcrt;
if MFOTL.in_interval (MFOTL.ts_minus tsq ptsq) intv then
Some rel1
else
Some Relation.empty
| None -> None
end
| ENext (intv,f1,inf) ->
if Misc.debugging Dbg_eval then
Printf.printf "[eval,Next] inf.init=%b\n%!" inf.init;
if inf.init then
begin
match eval f1 crt discard with
| Some _ -> inf.init <- false
| _ -> ()
end;
if Neval.is_last crt then
None
else
begin
let ncrt = Neval.get_next crt in
let nq, ntsq = Neval.get_data ncrt in
assert (nq = q+1);
match eval f1 ncrt discard with
| Some rel1 ->
if MFOTL.in_interval (MFOTL.ts_minus ntsq tsq) intv then
Some rel1
else
Some Relation.empty
| None -> None
end
| ESinceA (comp,intv,f1,f2,inf) ->
if Misc.debugging Dbg_eval then
Printf.printf "[eval,SinceA] q=%d\n%!" q;
let eval_f1 rel2 comp2 =
(match eval f1 crt false with
| Some rel1 ->
inf.sarel2 <- None;
Some (comp2 rel1 rel2)
| None ->
inf.sarel2 <- Some rel2;
None
)
in
let update_sauxrels = update_since_all intv tsq inf comp in
(match inf.sarel2 with
| Some rel2 -> eval_f1 rel2 update_sauxrels
| None ->
(match eval f2 crt false with
| None -> None
| Some rel2 -> eval_f1 rel2 update_sauxrels
)
)
| ESince (comp,intv,f1,f2,inf) ->
if Misc.debugging Dbg_eval then
Printf.printf "[eval,Since] q=%d\n" q;
let eval_f1 rel2 comp2 =
(match eval f1 crt false with
| Some rel1 ->
inf.srel2 <- None;
Some (comp2 rel1 rel2)
| None ->
inf.srel2 <- Some rel2;
None
)
in
let update_sauxrels = update_since intv tsq inf.sauxrels comp discard in
(match inf.srel2 with
| Some rel2 -> eval_f1 rel2 update_sauxrels
| None ->
(match eval f2 crt false with
| None -> None
| Some rel2 -> eval_f1 rel2 update_sauxrels
)
)
| EOnceA ((c,_) as intv, f2, inf) ->
(match eval f2 crt false with
| None -> None
| Some rel2 ->
if Misc.debugging Dbg_eval then
Printf.printf "[eval,OnceA] q=%d\n" q;
if c = CBnd MFOTL.ts_null then
begin
inf.ores <- Relation.union inf.ores rel2;
Some inf.ores
end
else
begin
if not (Relation.is_empty rel2) then
mqueue_add_last inf.oaauxrels tsq rel2;
update_once_all intv tsq inf;
Some inf.ores
end
)
| EAggOnce (inf, state, f) ->
(match eval f crt false with
| Some rel ->
state#update tsq rel;
Some (if discard then Relation.empty
else warn_if_empty_aggreg inf state#get_result)
| None -> None
)
(* We distinguish between whether the left margin of [intv] is
zero or not, as we need to have two different ways of
representing the margins of the windows in the tree: when 0
is not included we can use the timestamps and merge
relations at equal timestamps; otherwise, when 0 is not
included, we need to use the timepoints. *)
| EOnceZ (intv,f2,inf) ->
(match eval f2 crt false with
| None -> None
| Some rel2 ->
if Misc.debugging Dbg_eval then
Printf.printf "[eval,OnceZ] q=%d\n" q;
Some (update_once_zero intv q tsq inf rel2 discard)
)
| EOnce (intv,f2,inf) ->
(match eval f2 crt false with
| None -> None
| Some rel2 ->
if Misc.debugging Dbg_eval then
Printf.printf "[eval,Once] q=%d\n" q;
if not (Relation.is_empty rel2) then
dllist_add_last inf.oauxrels tsq rel2;
Some (update_once intv tsq inf discard)
)
| EUntil (comp,intv,f1,f2,inf) ->
(* contents of inf: (f = f1 UNTIL_intv f2)
ulast: last cell of neval for which both f1 and f2 are evaluated
ufirst: boolean flag indicating if we are at the first
iteration after the evaluation of f (i.e. q was
just moved); in this case we remove auxiliary
relations at old q
ures: the current partial result (for f)
urel2: the evaluation of f2 at ulast
raux, saux: the auxiliary relations
*)
if Misc.debugging Dbg_eval then
begin
let str = Printf.sprintf "[eval,Until] q=%d inf: " q in
print_uinf str inf
end;
if inf.ufirst then
begin
inf.ufirst <- false;
let (i,_) = Neval.get_data inf.ulast in
update_old_until q tsq i intv inf discard;
if Misc.debugging Dbg_eval then
print_uinf "[eval,Until,after_update] inf: " inf
end;
(* we first evaluate f2, and then f1 *)
let rec evalf1 i tsi rel2 ncrt =
(match eval f1 ncrt false with
| Some rel1 ->
update_until q tsq i tsi intv rel1 rel2 inf comp discard;
inf.urel2 <- None;
inf.ulast <- ncrt;
evalf2 ()
| None ->
inf.urel2 <- (Some rel2);
None
)
and evalf2 () =
if Neval.is_last inf.ulast then
None
else
let ncrt = Neval.get_next inf.ulast in
let (i,tsi) = Neval.get_data ncrt in
if not (MFOTL.in_left_ext (MFOTL.ts_minus tsi tsq) intv) then
(* we have the lookahead, we can compute the result *)
begin
if Misc.debugging Dbg_eval then
Printf.printf "[eval,Until] evaluation possible q=%d tsq=%s\n"
q (MFOTL.string_of_ts tsq);
let res = inf.ures in
inf.ures <- Relation.empty;
inf.ufirst <- true;
Some res
end
else
begin
(match inf.urel2 with
| Some rel2 -> evalf1 i tsi rel2 ncrt
| None ->
(match eval f2 ncrt false with
| None -> None
| Some rel2 -> evalf1 i tsi rel2 ncrt
)
)
end
in
evalf2()
| ENUntil (comp,intv,f1,f2,inf) ->
(* contents of inf: (f = NOT f1 UNTIL_intv f2)
ulast1: last cell of neval for which f1 is evaluated
ulast2: last cell of neval for which f2 is evaluated
listrel1: list of evaluated relations for f1
listrel2: list of evaluated relations for f2
NOTE: a possible optimization would be to not store empty relations
*)
(* evaluates the subformula f as much as possible *)
let rec eval_subf f list last =
if Neval.is_last last then
last
else
let ncrt = Neval.get_next last in
match eval f ncrt false with
| None -> last
| Some rel ->
(* store the result and try the next time point *)
let i, tsi = Neval.get_data ncrt in
Dllist.add_last (i, tsi, rel) list;
eval_subf f list ncrt
in
(* evaluate the two subformulas *)
inf.last1 <- eval_subf f1 inf.listrel1 inf.last1;
inf.last2 <- eval_subf f2 inf.listrel2 inf.last2;
(* checks whether the position to be evaluated is beyond the interval *)
let has_lookahead last =
let ncrt =
if Neval.is_last last then
last
else
Neval.get_next last
in
let _, tsi = Neval.get_data ncrt in
not (MFOTL.in_left_ext (MFOTL.ts_minus tsi tsq) intv)
in
if has_lookahead inf.last1 && has_lookahead inf.last2 then
(* we have the lookahead for both f1 and f2 (to be consistent with Until),
we can compute the result
NOTE: we could evaluate earlier with respect to f1, also in Until *)
begin
(* we iteratively compute the union of the relations [f1]_j
with q <= j <= j0-1, where j0 is the first index which
satisfies the temporal constraint relative to q *)
let f1union = ref Relation.empty in
let crt1_j = ref (Dllist.get_first_cell inf.listrel1) in
let rec iter1 () =
let j,tsj,relj = Dllist.get_data !crt1_j in
if j < q then
begin (* clean up from previous evaluation *)
assert (j = q-1);
ignore(Dllist.pop_first inf.listrel1);
crt1_j := Dllist.get_next inf.listrel1 !crt1_j;
iter1 ()
end
else if not (MFOTL.in_right_ext (MFOTL.ts_minus tsj tsq) intv) then
begin
f1union := Relation.union !f1union relj;
if not (Dllist.is_last inf.listrel1 !crt1_j) then
begin
crt1_j := Dllist.get_next inf.listrel1 !crt1_j;
iter1 ()
end
end
in
iter1 ();
(* we now iterate through the remaining indexes, updating the
union, and also computing the result *)
let res = ref Relation.empty in
let crt2_j = ref (Dllist.get_first_cell inf.listrel2) in
let rec iter2 () =
let j2,tsj2,rel2 = Dllist.get_data !crt2_j in
if j2 < q || not (MFOTL.in_right_ext (MFOTL.ts_minus tsj2 tsq) intv) then
begin (* clean up from previous evaluation *)
ignore(Dllist.pop_first inf.listrel2);
if not (Dllist.is_last inf.listrel2 !crt2_j) then
begin
crt2_j := Dllist.get_next inf.listrel2 !crt2_j;
iter2 ()
end
end
else
begin
let j1,tsj1,rel1 = Dllist.get_data !crt1_j in
assert(j1 = j2);
if MFOTL.in_left_ext (MFOTL.ts_minus tsj2 tsq) intv then
begin