-
Notifications
You must be signed in to change notification settings - Fork 4
/
README.keymaera
179 lines (138 loc) · 7.19 KB
/
README.keymaera
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
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
KeYmaera
--------
KeYmaera is a hybrid verification tool for hybrid systems that combines deductive, real
algebraic, and computer algebraic prover technologies. It is an automated and interactive
theorem prover for a natural specification and verification logic for hybrid systems.
KeYmaera supports differential dynamic logic (dL), which is a real-valued first-order
dynamic logic for hybrid programs, a program notation for hybrid automata. For automating
the verification process, KeYmaera implements a generalized free-variable sequent
calculus and automatic proof strategies that decompose the hybrid system specification
symbolically. To overcome the complexity of real arithmetic, we integrate real quantifier
elimination following an iterative background closure strategy. Our tool is particularly
suitable for verifying parametric hybrid systems and has been used successfully for
verifying collision avoidance in case studies from train control and air traffic
management.
Requirements
------------
- orbital-core.jar
- orbital-ext.jar
- ANTLR 3.4
- JLink from Mathematica
- scala 2.9+ from http:https://www.scala-lang.org/
- jmathplot
Required key-ext-jars libraries
-------------------------------
The directory key-ext-jars/ needs the following content (also see other README* files for KeY)
key-ext-jars/JLink -> /Applications/Mathematica.app/SystemFiles/Links/JLink/
key-ext-jars/antlr.jar (3.4+)
key-ext-jars/javacc.jar (version 4+)
key-ext-jars/junit.jar (version 4.4+)
key-ext-jars/log4j.jar
key-ext-jars/orbital-core.jar from http:https://symbolaris.com/orbital/
key-ext-jars/orbital-ext.jar from http:https://symbolaris.com/orbital/
key-ext-jars/recoderKey.jar
key-ext-jars/scala-library.jar from http:https://www.scala-lang.org/
key-ext-jars/jmathplot.jar from http:https://code.google.com/p/jmathplot/
In the above list "->" indicates a symlink. Paths may need to be adjusted depending on your operating system and platform.
NOTE that it is good practice when interacting with multiple branches on git to have a directory ../key-ext-jars with all the libraries and then use the following command
> cd keymaera
> ln -s ../key-ext-jars .
Compilation
-----------
> cd keymaera
> make -C system/ realclean all
Even though make is the preferred way, you can also try to compile KeYmaera using ant as follows
> cd keymaera/system
> ANT_OPTS="-Xms512m -Xmx512m" ant all
You can also set the environment variable and used
> export ANT_OPTS="-Xms512m -Xmx512m"
> cd keymaera/system
> ant all
Compilation Issues
------------------
If you see errors during compilation, check for the following issues.
1) make sure all the libraries in the key-ext-jars directory have *exactly* the right versions of the libraries in *exactly the right places*. Especially double check your different versions of antlr*.jar
2) Triple check that antlr is not loaded from other places instead of your key-ext-jars. Remove this and similar files if you experience problems during compilation.
3) For ant make sure that you have set SCALA_HOME as well as JAVA_HOME as environment variables
Startup
-------
Client:
The client side program can be started using the runKeYmaera script. You avoid problems by starting it from the keymaera directory
Example:
> bin/runKeYmaera
Server (optional):
The mathematica server can be started using the runMathematicaServer
script. You avoid problems by starting it from the keymaera directory
Example:
> bin/runMathematicaServer
Version Control
---------------
since it looks like a number of people here a struggling with
git, let me give some general notes and a bunch of links that can
help you dealing with the version control:
General pardigm: Git is distributed and everything VCS related
should be done _within_ the VCS.
That is, if you want to try out some things, then:
1. create a fresh branch: git branch maybeAGoodFeature
2. checkout this branch: git checkout maybeAGoodFeature
3. ... hack/code ...
4. ... compile ...
5. commit:
- git add <list of files you changed>
- git commit
6. ... test ...
7. maybe go back to 3
this way everything is documented in the VCS and if at some point
you decide that some change made it worse, you can just jump back
a commit (see git reset, an example would be git reset --hard HEAD~1).
If you want to check what is going on, on the stable branch, you
can do so at any point _after_ step 5. That means once your
changes are commited you could do the following:
6a. git checkout keymaeraStable
7a. git pull (this is git fetch origin && git merge origin/keymaeraStable)
If something interesting happend on the master branch that you
want on your new feature branch as well, you can do
git checkout maybeAGoodFeature
git fetch origin
git merge origin/keymaeraStable
like in any other VCS it might be that not all changes can be
merged automatically here. If there are conflicts, unlike in svn,
these are between already commited changesets. That means what
every you do (if you do not start rewriting the git history) you
will never loose your changes as you can always return to the
HEAD of your feature branch which contains the state before you
tried merging.
Once your new feature is ready or you want to show it to other
people you can push it to our common repository:
git push origin maybeAGoodFeature:refs/heads/keymaeraGoodFeature
and write a mail: "Hey, check out my cool feature. You can do
git fetch origin
git checkout -b maybeAGoodFeature origin/keymaeraGoodFeature --track
to test it. Enjoy."
Once, the feature is ready I will then merge it into the stable
branch so that it becomes easily available to all users.
So, to sum up git: branching is cheap and cool.
A cheat sheet with a short overview about the commands:
http:https://byte.kde.org/~zrusin/git/git-cheat-sheet-medium.png
For users that are already familiar with SVN:
http:https://git.or.cz/course/svn.html
http:https://www.ibm.com/developerworks/linux/library/l-git-subversion-1/
General git guides/howtos:
http:https://rogerdudler.github.com/git-guide/
http:https://stackoverflow.com/questions/315911/git-for-beginners-the-definitive-practical-guide
http:https://git-scm.com/book
If you are familiar with a different version control system,
usually a quick google search for "git guide <vcs name>" will
bring up a pretty good guide.
Hope this helps with dealing with git.
Adding additional Backends
--------------------------
What do I need to do to get listed on this startup prompt? Here is what I have done:
1. Created appropriate entries in system/de/uka/ilkd/key/dl/options/EPropertyConstant.java
2. Made system-specific default functions like everybody else in system/de/uka/ilkd/key/dl/gui/initialdialog/defaultsettings/[LinuxOs,WindowsOs,MacOs]DefaultProperties.java
3. Made an entry in system/de/uka/ilkd/key/dl/gui/initialdialog/defaultsettings/OsDefaultProperties.java, in getDefaultPropertyList, I added props.put(EPropertyConstant.MATLAB_OPTIONS_BINARY etc..
4. In this same file, made a call to getMatlabBinaryPath() in the same style as everybody else, which in my understanding should make the appropriate call depending on the OS
you need a bean to read the information (see
de.uka.ilkd.key.dl.arithmetics.impl.redlog.Options for example) and
configure that it is used in system/resources/hybridkey.xml.
further, add an entry to de.uka.ilkd.key.dl.gui.initialdialog.propertyconfigurations.EPropertyConfigurations