forked from imitator-model-checker/imitator
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathoasis-config
71 lines (56 loc) · 2.75 KB
/
oasis-config
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
###############################################################
#
# IMITATOR
#
# Laboratoire Specification et Verification (ENS Cachan & CNRS, France)
# Laboratoire d'Informatique de Paris Nord (Paris 13, France)
#
# _oasis authors: Etienne Andre, Alban Linard
# Created: 2013/12/11
# Last modified: 2015/04/23
###############################################################
OASISFormat: 0.3
Name: IMITATOR
Version: 2.6.3
Synopsis: shortdescription
Authors: Etienne Andre, Ulrich Kuehne et al.
License: GPL-3.0
# Handling build number (using Python)
PreBuildCommand: python gen_build_info.py
PostBuildCommand: python incrementer.py ; echo "Copying main binary file to bin/imitator ..." ; cp _build/src/IMITATOR.native bin/imitator
Executable imitator
Path: .
BuildTools: ocamlbuild
MainIs: src/IMITATOR.ml
BuildDepends: gmp, extlib, mpi, ppl, str, unix, threads
CCLib: -lstdc++
# -ltinfo
# CCLib: -static '-lppl -ltinfo -lppl_ocaml -lstdc++ -lgmp -lgmpxx -lmpi'
# CCLib: -static '-lppl -ltinfo -lppl_ocaml -lstdc++ -lgmp -lgmpxx -llam -llamf77mpi -llammpi++ -llammpio -lmpi -lcamlmpi'
# -static to have a static compiling (+ ' ' around)
# I removed -lcamlrun because I wrote "best" instead of "byte"
CompiledObject: best
Test startingcomment
Command: echo "\n********** STARTING TESTS **********\n"
Test tes1
Command: echo "\n********** TEST 1 **********\n"; \
./bin/imitator examples/Flipflop/flipflop.imi -mode statespace -depth-limit 5
Test test2
Command: echo "\n********** TEST 2 **********\n"; \
./bin/imitator examples/Flipflop/flipflop.imi examples/Flipflop/flipflop.pi0 -output-trace-set -output-states -output-result -statistics
Test test3
Command: echo "\n********** TEST 3 **********\n"; \
./bin/imitator examples/Flipflop/flipflop.imi examples/Flipflop/flipflop.v0 -mode cover -output-cart
Test test4
Command: echo "\n********** TEST 4 **********\n"; \
./bin/imitator examples/Examples/JLR-TACAS13.imi examples/Examples/JLR-TACAS13.v0 -mode cover -PRP -output-result -output-cart -depth-limit 10 -verbose warnings
Test test5
Command: echo "\n********** TEST 5 **********\n"; \
mpiexec -n 4 ./bin/imitator examples/Flipflop/flipflop.imi examples/Flipflop/flipflop.v0 -mode cover -output-cart -distributed sequential -verbose standard
Test test6
Command: echo "\n********** TEST 6 **********\n"; \
mpiexec -n 4 ./bin/imitator examples/Flipflop/flipflop.imi examples/Flipflop/flipflop.v0 -mode cover -output-result -output-cart -distributed dynamic -verbose mute
Test finalcomment
Command: echo "\n********** END TESTS **********\n"
# THE MAIN COMMAND TO COMPILE OASIS IS:
# oasis setup && ocaml setup.ml -configure --enable-tests && ocaml setup.ml -all