Commit 337378d3 authored by Benoit Barbot's avatar Benoit Barbot
Browse files

add coverage

parent f0d4ceb4
Pipeline #1700 failed
......@@ -7,6 +7,7 @@ before_script:
stages:
- build
- test
- deploy
pages:
......@@ -30,6 +31,14 @@ pages:
# tags:
# - darwin
test:
stage:test
script:
- make test
artifacts:
paths:
- test/_coverage
wordgen-linux:
stage: build
script:
......
......@@ -3,9 +3,15 @@ all:
cp src/wordgen.native wordgen
test: all
export OCAMLRUNPARAM=b; ./wordgen example/simpleTriAngle.prism
test:
cd src; BISECT_COVERAGE=YES ocamlbuild -use-ocamlfind -plugin-tag 'package(bisect_ppx-ocamlbuild)' wordgen.native
cd test; ./integration.sh
cd test; bisect-ppx-report html --source-path ../src/_build
cd test; bisect-ppx-report summary
clean:
cd src; ocamlbuild -clean
rm test/*.coverage
rm wordgen
.PHONY : clean test all
......@@ -188,7 +188,7 @@ module Make (Bt:BoundType) =
let zg = ZoneGraph.of_json j in
if verbose >0 then printf "%i states found. [%.2fs]\n" (Array.length zg.ZoneGraph.statelist) (check_time ());
(*zg*)
failwith "do not use"
failwith "json parser deprecated"
| ".xml" | ".prism" ->
(* Input is a time automaton in prism or UPPAAL file format *)
let ta = try if e = ".xml" then
......
true:debug
true:debug, coverage
"flq.ml":package(zarith)
"fl.ml":package(num)
"symrob_extract/uppaal_parser/utaReader.ml":package(xml-light)
......
let () = Ocamlbuild_plugin.Options.use_ocamlfind := true
open Ocamlbuild_plugin
let () = Options.use_ocamlfind := true
let _ =
Bisect_ppx_plugin.handle_coverage ()
(*let () = Ocamlbuild_plugin.dispatch Ocamlbuild_js_of_ocaml.dispatcher*)
open Printf
type log_t = Info | Debug | Warning | Error | Fatal
let log_level = ref Debug
let set_level level = log_level := level
let log_err_channel = stderr
let log_regular_channel = stdout
let logf level s f =
(match level with
| Error ->
Printf.fprintf log_err_channel "[ERR] ";
Printf.fprintf log_err_channel s f
| Fatal ->
Printf.fprintf log_err_channel "[FAT] ";
Printf.fprintf log_err_channel s f;
exit(-1)
| Warning ->
if ( !log_level = Debug || !log_level = Warning ) then
(
Printf.fprintf log_err_channel "[WAR] ";
Printf.fprintf log_err_channel s f
)
| Info ->
if ( !log_level = Info || !log_level = Debug || !log_level = Warning ) then
(
Printf.fprintf log_regular_channel "[INF] ";
Printf.fprintf log_regular_channel s f
)
| Debug ->
if ( !log_level = Debug ) then
(
Printf.fprintf log_regular_channel "[DEB] ";
Printf.fprintf log_regular_channel s f;
)
);
flush log_err_channel;
flush log_regular_channel
let fatal s =
logf Fatal "%s" s
let info s =
logf Info "%s" s
let warning s =
logf Warning "%s" s
let infof f s =
logf Info f s
let warningf f s =
logf Warning f s
let fatalf f s =
logf Fatal f s
let debug s =
logf Debug "%s" s
let debugf f s =
logf Debug f s
let log level s =
logf level "%s" s
module SearchStatistics =
struct
let counter_visited = ref 0
let counter_gamma = ref 0
let counter_acceleration = ref 0
(** Number of iterations of the binary search *)
let counter_bsiterations = ref 0
let increment_visited () = incr(counter_visited)
let increment_gamma () = incr(counter_gamma)
let increment_acceleration () = incr(counter_acceleration)
let reset_counters () =
counter_visited := 0;
counter_gamma := 0;
counter_acceleration := 0;
counter_bsiterations := 0
let print_statistics chan mode =
match mode with
Options.ExactReachability
| Options.Verifix ->
fprintf chan "[INF] Search Statistics:\n";
fprintf chan "[INF] Visited states: %d\n" !counter_visited
|Options.RobustReachability ->
fprintf chan "[INF] Search Statistics:\n";
fprintf chan "[INF] Visited states: %d\n[INF] Expanded gamma cycles: %d (%d new states)\n" !counter_visited !counter_acceleration !counter_gamma
end
......@@ -597,7 +597,7 @@ struct
Dbm.posttime z;
let inv = (invariant_of_discrete_state ta ta.init) in
Dbm.intersect z inv
with EmptyDBM -> Log.fatal "The initial state is empty\n"
with EmptyDBM -> failwith "The initial state is empty\n"
| _ as e-> raise e
);
(ta.init, z)
......
WG=../src/wordgen.native
$WG ../example/nfm19.prism
$WG ../example/nfm19.prism --traj 100 --receding 10
$WG ../example/nfm19.prism --frequency 1.0
$WG ../example/nfm19.prism --frequency 1.0 --exact-rational
$WG ../example/nfm19.prism --time-duration 1.0
$WG ../example/nfm19.prism --time-duration 1.0 --exact-rational
$WG ../example/test2mod.prism out.dat
$WG ../example/test2mod.prism --frequency 1
$WG ../example/test2mod.prism --time-duration 9 --exact-rational
$WG ../example/bimodal.prism --time-duration 4.4
$WG ../example/nfm19.prism --template "@1[b]0.2[0.3]_[_]"
$WG ../example/nfm19.prism --template "@1[b]0.2[0.3]_[_]" --poly -1
$WG ../example/nfm19.prism --debug --output-format debug --splitting-debug test.tex
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment