Skip to content

Commit 7796f22

Browse files
author
Ioana
committed
start using the replay
1 parent 10bcbcc commit 7796f22

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

43 files changed

+270
-4369
lines changed

_tags

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,2 @@
1-
true: package(yojson), package(z3)
1+
true: package(yojson), package(z3), package(KappaLib)
22
true: debug, bin_annot

ast.ml

Lines changed: 0 additions & 188 deletions
This file was deleted.

ast.mli

Lines changed: 0 additions & 36 deletions
This file was deleted.

concret.ml

Lines changed: 10 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -1,42 +1,24 @@
11
let linears s =
22
LinearPoset.linearisations(s)
33

4-
let concretise (s:LinearPoset.t) (rs:Rule.t list) =
5-
let () = if (!Parameter.debug_mode) then
4+
let concretise (s:LinearPoset.t) =
5+
let () = if (!Param.debug_mode) then
66
(Format.printf "concretise linear poset :";
77
List.iter (fun i -> Format.printf "%d " i) s.LinearPoset.seq) in
88
let (trace,_) =
99
List.fold_left
1010
(fun (trace,rf) eid ->
1111
let event = Poset.get_event_by_id eid s.LinearPoset.pos in
12-
let rname = Event.get_label event in
13-
let rule = Rule.get_rule_by_label rname rs in
14-
let m = Transition.get_rhs (Trace.get_first_transition trace) in
12+
let step = Event.get_step event in
13+
let m = Transition.get_rhs (TraceConcret.get_first_transition trace) in
1514
let (trans,new_nodes,new_ports) =
16-
Transition.make m rule (Event.get_quarks event)
17-
trace.Trace.node_names trace.Trace.port_names in
18-
((Trace.add_transition trace trans new_nodes new_ports),
15+
Transition.make m step
16+
trace.TraceConcret.node_names
17+
trace.TraceConcret.port_names in
18+
((TraceConcret.add_transition trace trans new_nodes new_ports),
1919
((eid,trans)::rf)))
20-
(Trace.empty,[]) s.LinearPoset.seq in
20+
(TraceConcret.empty,[]) s.LinearPoset.seq in
2121
trace
2222

23-
(*let test_concret (s:LinearPoset.t) (rs:Rule.t list) =
24-
let () = if (!Parameter.debug_mode) then
25-
(Format.printf "concretise linear poset :";
26-
List.iter (fun i -> Format.printf "%d " i) s.LinearPoset.seq) in
27-
let event = Poset.get_event_by_id 4 s.LinearPoset.pos in
28-
let rname = Event.get_label event in
29-
let rule = Rule.get_rule_by_label rname rs in
30-
31-
let () = if (!Parameter.debug_mode) then
32-
(Format.printf "info on first event ";
33-
Event.print_event event;
34-
Rule.print rule) in
35-
36-
let (trans,_,_) = Transition.make [] rule (Event.get_quarks event) [] [] in
37-
let () = if (!Parameter.debug_mode) then
38-
Transition.print trans in
39-
Trace.empty
40-
*)
4123

42-
let concret (s:Poset.t) (rs:Rule.t list) = concretise (linears s) rs
24+
let concret (s:Poset.t) = concretise (linears s)

concret.mli

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,2 @@
11

2-
val concret : Poset.t -> Rule.t list -> Trace.t
2+
val concret : Poset.t -> TraceConcret.t

domain.ml

Lines changed: 6 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -22,12 +22,8 @@ let get_poset_from_filename s dlist =
2222

2323
let print_posets t =
2424
List.iteri
25-
(fun i p -> Format.printf "\n poset nb %d\n" i; Poset.print_poset p)
26-
t.poset_list;
27-
Format.printf "events: \n";
28-
List.iteri
29-
(fun i e -> Format.printf "event nb %d \n" i; Event.print_event e)
30-
t.event_list
25+
(fun i p -> Format.printf "\nposet nb %d\n" i; Poset.print_poset p)
26+
t.poset_list
3127

3228
let print_domain = function
3329
| Pos p -> (match p.Poset.filename with
@@ -39,20 +35,18 @@ let print_domain_list l =
3935
List.iter (fun d -> print_domain d) l;
4036
Format.printf"\n"
4137

42-
4338
let add_posets p current_posets =
4439
{ poset_list = p::current_posets.poset_list;
4540
event_list = p.Poset.events@current_posets.event_list; }
4641

47-
let set_posets file_list =
42+
let set_posets file_list sigs =
4843
let posets : t = { poset_list = []; event_list = []; } in
4944
let posets_file =
5045
List.fold_left
5146
(fun t file ->
52-
let s = Poset.read_poset_from_file file in
47+
let s = Poset.read_poset_from_file file sigs in
5348
add_posets s t) posets file_list in
54-
(*let posets' = add_posets (Poset.test_poset) posets_file in*)
55-
let () = if (!Parameter.debug_mode)
56-
then (Format.printf "set_posets: \n";
49+
let () = if (!Param.debug_mode)
50+
then (Format.printf "\nset_posets";
5751
print_posets posets_file) in
5852
posets_file

domain.mli

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,6 @@ val print_posets: t -> unit
1515
val print_domain : domain -> unit
1616
val print_domain_list : domain list -> unit
1717

18-
val set_posets : string list -> t
18+
val set_posets : string list -> Model.t -> t
1919

2020
val get_poset_from_filename : string -> domain list -> domain

0 commit comments

Comments
 (0)