Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / GMLMIP-0.1 / README.txt @ 7c4d2eb4

History | View | Annotate | Download (2.6 KB)

1
===============================
2
Author: William Snell
3
Check http://project.williamsnell.co.uk for future updates.
4
================================
5

    
6
Requirements:
7

    
8
GNU LPK, Flex, Bison, Googlesparsehash package, BuDDy BDD package.
9

    
10
(Extensively tested with GNU-LPK 4.38)
11

    
12
=================================
13
Compiling:
14

    
15
To compile you will need to edit the makefiles in the sub-folders and this folder to point to the location of your compiler/bison/flex. 
16

    
17
Also need to edit the include directory and linking directories in all 4 make files to point to where you have installed GLPK, sparsehash and BuDDy. If you install these properly in /bin /usr (unlike the lab set-up) you should be able to just remove these parts and have it compile fine.
18

    
19
Then if you run the compile.sh script, everything should compile properly for you.
20

    
21
=================================
22
Usage:
23

    
24
Input is written in a separate file and then this file is is passed as an argument on the command line.
25

    
26
./main input
27

    
28
You can use the -v flag for output. At each step of the top level tableau calculus algorithm it tells you how many satisfying assignments and how many rules it has found.
29

    
30
Included is Dmitry V Golovashkin's timeout script. The following would run the program on the input file with a timeout of 300 seconds.
31
 
32
./timeoutwrapper.sh -t 300 ./src/main input
33

    
34

    
35
=================================
36
Input file specification:
37

    
38
First we specify which logic then use the following notation:
39

    
40
<a> GML diamond ('more than a successors ...')
41
[a] GML box     ('fails at most a times ...')
42
<a/b> PML diamond
43
[a/b] PML box
44
~ not
45
v or
46
& and
47
(
48
)
49

    
50
Examples:
51

    
52
Logic:PML
53
<1/2>p0 & ~<1/4>p2 v [1/8]p3
54

    
55
Logic:GML
56
<1>p0 & <1>(p0 v p0)
57

    
58

    
59
=================================
60
Known Issues & Notes:
61

    
62
1) The following warning is generated by the C code generated by flex.
63
	position.hh:136: warning: suggest parentheses around ‘&&’ within ‘||’
64

    
65
2) Use of deprecated header <ext/hash_map>.
66

    
67
3) You may need to alter the line "using __gnu_cxx::hash;" line in formula.h depending on your compiler. 
68

    
69
4) I received "./main: error while loading shared libraries: libbdd.so.0: cannot open shared object file: No such file or directory" errors. 
70
Fixed by adding "export LD_LIBRARY_PATH=~/lib/lib:$LD_LIBRARY_PATH" to my .bashrc file. Where ~/lib/lib is where I locally installed the required libraries. (No root access for lab machines.)
71

    
72
5) If you receive error "BDD error: unknown variable" you have not declared enough variables in the BDD initialisation in main.cpp. The line "bdd_setvarnum(int)" needs increasing. 
73

    
74
6) What report describes as TruthAssignment class is implemented as Valuation.
75

    
76

    
77

    
78

    
79