-
Notifications
You must be signed in to change notification settings - Fork 12
/
Copy pathoasis-config-distr
76 lines (60 loc) · 2.96 KB
/
oasis-config-distr
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
###############################################################
#
# IMITATOR
#
# Laboratoire Specification et Verification (ENS Cachan & CNRS, France)
# Université Sorbonne Paris Nord, LIPN, CNRS, France
# Université de Lorraine, CNRS, Inria, LORIA, Nancy, France
#
# _oasis authors: Étienne André, Alban Linard
# Created: 2013/12/11
# Last modified: 2022/10/17
###############################################################
OASISFormat: 0.3
Name: PaTATOR
Version: 3.1
Synopsis: shortdescription
Authors: Étienne André et al.
License: GPL-3.0
# Handling build number (using Python)
PreBuildCommand: python gen_build_info.py
PostBuildCommand: echo "Copying main binary file to bin/patator …" ; cp _build/src/PaTATOR.native bin/patator ; strip bin/patator
Executable patator
Path: .
BuildTools: ocamlbuild
MainIs: src/PaTATOR.ml
BuildDepends: gmp, extlib, mpi, ppl, str, unix, threads, bytes, fileutils
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/patator tests/testcases/flipflop.imi -mode statespace -depth-limit 5
#Test test2
# Command: echo "\n********** TEST 2 **********\n"; \
# ./bin/patator tests/testcases/flipflop.imi tests/testcases/flipflop.pi0 -draw-statespace normal -states-description -statistics
#Test test3
# Command: echo "\n********** TEST 3 **********\n"; \
# ./bin/patator tests/testcases/flipflop.imi tests/testcases/flipflop-cover.imiprop -draw-cart
#Test test4
# Command: echo "\n********** TEST 4 **********\n"; \
# ./bin/patator tests/testcases/JLR-TACAS13.imi tests/testcases/JLR-TACAS13-PRPC.imiprop -draw-cart -depth-limit 10 -verbose warnings
#Test test5
# Command: echo "\n********** TEST 5 **********\n"; \
# mpiexec -n 4 ./bin/patator tests/testcases/flipflop.imi tests/testcases/flipflop-cover.imiprop -draw-cart -distributed sequential -verbose standard
#Test test6
# Command: echo "\n********** TEST 6 **********\n"; \
# mpiexec -n 4 ./bin/patator tests/testcases/testBC-grid-plain.imi tests/testcases/testBC-grid3x3-cover.imiprop -draw-cart -distributed dynamic -verbose low
#Test test7
# Command: echo "\n********** TEST 7 **********\n"; \
# mpiexec -n 4 ./bin/patator tests/testcases/flipflop.imi tests/testcases/flipflop-cover.imiprop -draw-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