ls-lab / keymaerax-release Goto Github PK

KeYmaera X: An aXiomatic Tactical Theorem Prover for Hybrid Systems (release)

License: GNU General Public License v2.0

Scala 69.71% Java 0.05% CSS 0.88% HTML 3.30% JavaScript 21.08% Perl 0.01% Shell 0.04% C 0.04% Mathematica 4.86% Dockerfile 0.03%

hybrid-systems theorem-prover dynamic-logics dynamical-systems proof tactics mathematica differential-dynamic-logic differential-equations axiom

keymaerax-release's People

Contributors

Stargazers

Watchers

keymaerax-release's Issues

STTT 9b fails due to substitution clash

Around commit f96b147

The stack trace that you get from "details" does not close when you close the error message

in the prover interface

/show links broken

/show links do not work even when the associated model/proof work when manually executed. Possibly relevant warning message:

[WARN] [09/22/2017 18:44:38.291] [on-spray-can-akka.actor.default-dispatcher-5] [akka://on-spray-can/user/hydra] File-system path for base [] and Uri.Path [user/classpath:%2Fkeymaerax-projects%2Fitp17%2Fskydiver.kya/guest/mode/0] contains suspicious path segment [classpath:/keymaerax-projects/itp17/skydiver.kya], GET access was disallowed

Ensure that the templates are up to date

E.g., CheatSheet.kyx.proof instead of CheatSheet.kyp.

Proper parser for Archives/Lemmas

Replace the Regex-based stand-in with a proper parser (in the style of KeYmaera X parser or the Bellerophon parser).

Login fails when no username is provided

Invalid REST request is made instead of some sort of indicator telling you to log in. Confused students.

ASCII/.kyx extraction

There should be a way of extracting the current subgoal or a highlighted formula to ASCII / a .kyx file. The latter would require pretty-printing variable/function declarations (or just copying them from the input file).

JAR file name should not contain version number

The JAR files created by sbt assembly shouldn't change names between version udpates. Doing so creates too much documentation and usability overhead (especially because old JAR files stay around).

solve fails sometimes on constant functions

The solve tactic sometimes fails on inputs like

x'=v,v'=a*b

for a,b as functions even when it does not fail on

x'=v,v'=a*b

for a,b as program variables.

Loop inv rule not in hybrid programs dropdown menu

in the prover interface

ODE solve gives a truly cryptic error message in cases where it can't prove that the ODE doesn't divide by zero

e.g. doing solve on x > 0 & v > 0 & r > 0 |- [{x' = v / r}]x > 0 gives a truly inscrutable error message about not being able to prove some random stuff.

Tactic names in the Spinner dialog are sometimes wrong

For example, sometimes you'll run normalize and the text will say DC+DI. Do not know how to reproduce.

Import utility is broken

The import utility is broken.

point-to-prove equiv rewriting with auto-\forall-instantiation

It should be possible to drag-and drop formulas like \forall x p(x) <-> q(x) onto formulas like p(z) or q(z) and obtain the desired result. Ditto for formulas that do not have quantifiers.

URI limit prevents long loop invariants

From a very, very long loop invariant: URI length exceeds the configured limit of 2048 characters

dG broken in web ui again

Probably a derivation info bug. This was fixed prior to 4.3.11 but is back in 4.3.12.

axiomaticSove/diffSolve does not work with function definitions

E.g. ACAS X with Cimpl in post condition.

dG y'=y does not work

Mathematica setup suggests wrong directory for "Default Configuration" on Linux

With Mathematica 11.2 installed, KeYmaera X still suggests some /.../11.0 directory.

Log off button

Particularly needed now in light of 3a72b14

"You can log-off any time you want, but you can never leave" - ghc 3001 whiteboard

Should run database upgrade scripts during SSLBoot

Currently database migration is only run during non-SSL Boot, which means that the web server requires manual updates.

(novice question) Automatic prove does not do anything.

Hi there,

Thanks for for sharing a great project. I am trying to learn CPS verification (without prior knowledge on formal verification), and this one seems to be the most promising for my purpose among all candidates I tried.

However, I am having trouble with running a basic custom example, which is a room temperature controller. There is a temperature controller which controls temperature based on P controller where error is setpoint-temp. I would like to guarantee that the temperature is in a certain range (larger than 10C in the below example.)

This is my kyx file:

ProgramVariables.                                                               
R control_sig.                                                                           
R temp.                                                                           
R diff.                                                                            
R temp_setpoint.                                                                           
End.                                                                            
                                                                                
Problem.                                                                        
control_sig=50 &                                                                         
temp=18 &                                                                         
temp_setpoint=23                                                                           
->                                                                              
[                                                                               
{                                                                               
  {diff:=temp_setpoint-temp;}                                                                
  {temp_setpoint:=diff*0.5;}                                                               
  {temp'=0-control_sig*0.01}                                                               
}*@invariant(temp>10)                                                             
]                                                                               
(temp>10)                                                                         
End.

The model is accepted by the KeYmaera X, but when I try to prove it, it shows nothing. What I did is:
i) "Start new proof" for the model
ii) Click "Auto"
iii) It generates the following Tactic: master ; <(nil, nil )
I exported it and it is:

ArchiveEntry "test".                                                            
                                                                                
ProgramVariables.                                                               
R controlsig.                                                                   
R temp.                                                                         
R diff.                                                                         
R setpoint.                                                                     
End.                                                                            
                                                                                
Problem.                                                                        
controlsig=50 &                                                                 
temp=18 &                                                                       
setpoint=23                                                                     
->                                                                              
[                                                                               
{                                                                               
  {diff:=setpoint-temp;}                                                        
  {setpoint:=diff*0.5;}                                                         
  {temp'=0-controlsig*0.01}                                                     
}*@invariant(temp>10)                                                           
]                                                                               
(temp>20)                                                                       
End.                                                                            
                                                                                
                                                                                
Tactic "test: Proof 2".                                                         
  master                                                                        
End.                                                                            
                                                                                
                                                                                
End.

It did master tactic (which seems to be default built-in tactic), but the proof is not complete.

I thought that I provided enough information for the simple system, but ***what should I provide more? *** I am running it with Mathematica 11.1 on Ubuntu 16.04 64 bits.

I tried to follow the syntax doc, but please let me know if there is any reference that I can use as a beginner.

Thank you so much.

Provable/Lemma management in Web UI

It should be possible to extract a subgoal, prove that subgoal in another window, save the proven subgoal as a lemma, and then use the proven lemma in your original proof.

Note that this functionality already exists in the core+tactics language (proveAs/lazyUseAt or simply useAt), but isn't exposed to the web UI. Integrating with HyDRA so that the lemma cache is repopulated on-demand would also be nice.

1. Saving Lemmas

Add a "Save As Lemma" option in the drop-down menu on the proofs-of-model page, which allows saving the lemma with a name.
Add a lemmas table that stores the name, conclusion, and proofId of each lemma.
Add a mechanism for re-proving saved lemmas and then storing them in the lemma database (should do nothing if the lemma already exists in the lemma database and matches the expected conclusion). reProve(lemmaId)
Run this mechanism on every available lemma on server startup.

2. Using Lemmas

Add a tactic for using a lemma and expose this to the web ui.
Add a new REST request for running a lemma. If the lemma does not exist in the lemma database but does exist in the lemmas table, try to reProve(lemmaName).
- Add an element to the "Propositional" drop-down menu in the web ui. When clicked, search all elements of the lemmas table for something that matches the current subgoal. Prove by a useAt, doing a reProve(lemmaname) if there's a correct conclusion in the database but not in the lemma cache. Display errors otherwise "Current goal does not match conclusion of indicated lemma", or "Indicated lemma does not exist", or "failed to re-prove lemmaname: your proof of poofIdHere was deleted or no longer works in the latest version of KeYmaera X".

Temporary session w/ archive

Provide a REST call that creates a temporary session, logs the user in, loads an archive, and shows the user the model page. @smitsch @aplatzer

EquivRewriting sometimes fails with new unification

See the ignored rests cases in the EquivRewriting tests.

I think this happens because new unification requires subst over rename, but equiv rewriting requires renaming above subst (otherwise subst gets too clever).

Better failure messages for dI

E.g.

"Could not prove that the invariant holds initially: Ante ==> BLAH"

Or:

"Could not prove that the invariant is differentially inductive: 

Ante ==> [{ODE}](BLAH)'. 

FYI: (BLAH)' = insert derive(BLAH) here

Improved busy-waiting for web ui

This is silly when all we're doing is displaying a status window for a long-running task:

I'm not sure if we should switch to web sockets or maybe just taper off polling until getting to once or twice a second. There may be other ways to decrease memory and cpu usage as well.

DV differential variant >= needs a tactic

That does derive and so on as cleanup.

UI/Tactics ideas from today

Built-in chase-type guy that breaks stuff up into control choices nicely.
Improved documentation/naming for tactics library, especially differential stuff.
Remove *@ TheType() annotations

SQLite lemma db and File lemma db cannot have some interface

The file lemma db allows arbitrary id's while the sqlite lemma db does not.

We should change the sqlite lemma DB to use UNIQUE ID's that aren't necessary auto-increment integers.

sbt assembly sets wrong symlink to keymaerax.jar

after compiling the new version, the symlink of keymaerax.jar got updated to nfulton personal path.

fool@bar:~/keymaerax$ ls -l keymaerax.jar
lrwxr-xr-x 1 kghorbal staff 102 Apr 21 20:15 keymaerax.jar -> /home/nfulton_unencrypted/KeYmaeraX/keymaerax-webui/target/scala-2.11/KeYmaeraX-Web-assembly-4.3.8.jar

LMPC Tactics

See https://github.com/LS-Lab/KeYmaeraX/issues/118

Unprimed program variables occur in conclusion after running diffInd

The diffInd tactic does not add x'=0 for programVariables that do not occur primed in an ODE. This may affect other differential tactics.

To Reproduce, run implyR(1) & diffInd(1) on this model:

ProgramVariables.
  R x.
  R y.
End.
Problem.
  y>=0 -> [{x'=y}](y>=0)
End.

Edit: The solution isn't to literally add x'=0 but rather to consttify. Note that this was working properly in 4.1b2.

Edit 2: A temporary workaround is to add x' = 0 to your model for all non-primed programVariables.

08-events.kyx with invariant 0<=x

@aplatzer

Intermittant JVM error on startup

Possibly related to JLink.

/usr/lib/jvm/default-java/bin/java -Didea.launcher.port=7538 -Didea.launcher.bin.path=/home/nfulton/local_bin/2016_04_01/bin -Dfile.encoding=UTF-8 -classpath /home/nfulton/.IntelliJIdea2016.1/config/plugins/Scala/lib/scala-plugin-runners.jar:/usr/lib/jvm/default-java/jre/lib/charsets.jar:/usr/lib/jvm/default-java/jre/lib/compilefontconfig.jar:/usr/lib/jvm/default-java/jre/lib/ext/dnsns.jar:/usr/lib/jvm/default-java/jre/lib/ext/icedtea-sound.jar:/usr/lib/jvm/default-java/jre/lib/ext/java-atk-wrapper.jar:/usr/lib/jvm/default-java/jre/lib/ext/localedata.jar:/usr/lib/jvm/default-java/jre/lib/ext/sunjce_provider.jar:/usr/lib/jvm/default-java/jre/lib/ext/sunpkcs11.jar:/usr/lib/jvm/default-java/jre/lib/ext/zipfs.jar:/usr/lib/jvm/default-java/jre/lib/javazic.jar:/usr/lib/jvm/default-java/jre/lib/jce.jar:/usr/lib/jvm/default-java/jre/lib/jsse.jar:/usr/lib/jvm/default-java/jre/lib/management-agent.jar:/usr/lib/jvm/default-java/jre/lib/resources.jar:/usr/lib/jvm/default-java/jre/lib/rhino.jar:/usr/lib/jvm/default-java/jre/lib/rt.jar:/home/nfulton/dev/KeYmaeraX/keymaerax-webui/target/scala-2.11/test-classes:/home/nfulton/dev/KeYmaeraX/keymaerax-webui/target/scala-2.11/classes:/home/nfulton/dev/KeYmaeraX/keymaerax-core/target/scala-2.11/classes:/home/nfulton/.ivy2/cache/org.xerial/sqlite-jdbc/jars/sqlite-jdbc-3.7.2.jar:/home/nfulton/.ivy2/cache/org.slf4j/slf4j-api/jars/slf4j-api-1.7.5.jar:/home/nfulton/.ivy2/cache/org.scalatest/scalatest_2.11/bundles/scalatest_2.11-2.2.4.jar:/home/nfulton/.ivy2/cache/org.scalamock/scalamock-scalatest-support_2.11/jars/scalamock-scalatest-support_2.11-3.2.jar:/home/nfulton/.ivy2/cache/org.scalamock/scalamock-core_2.11/jars/scalamock-core_2.11-3.2.jar:/home/nfulton/.ivy2/cache/org.scala-lang.modules/scala-xml_2.11/bundles/scala-xml_2.11-1.0.4.jar:/home/nfulton/.ivy2/cache/org.scala-lang.modules/scala-parser-combinators_2.11/bundles/scala-parser-combinators_2.11-1.0.4.jar:/home/nfulton/.ivy2/cache/org.scala-lang/scala-reflect/jars/scala-reflect-2.11.7.jar:/home/nfulton/.ivy2/cache/org.scala-lang/scala-library/jars/scala-library-2.11.7.jar:/home/nfulton/.ivy2/cache/org.scala-lang/scala-compiler/jars/scala-compiler-2.11.7.jar:/home/nfulton/.ivy2/cache/org.pegdown/pegdown/jars/pegdown-1.5.0.jar:/home/nfulton/.ivy2/cache/org.parboiled/parboiled-scala_2.11/bundles/parboiled-scala_2.11-1.1.6.jar:/home/nfulton/.ivy2/cache/org.parboiled/parboiled-java/jars/parboiled-java-1.1.7.jar:/home/nfulton/.ivy2/cache/org.parboiled/parboiled-core/jars/parboiled-core-1.1.7.jar:/home/nfulton/.ivy2/cache/org.parboiled/parboiled-core/bundles/parboiled-core-1.1.6.jar:/home/nfulton/.ivy2/cache/org.ow2.asm/asm-util/jars/asm-util-5.0.3.jar:/home/nfulton/.ivy2/cache/org.ow2.asm/asm-tree/jars/asm-tree-5.0.3.jar:/home/nfulton/.ivy2/cache/org.ow2.asm/asm-analysis/jars/asm-analysis-5.0.3.jar:/home/nfulton/.ivy2/cache/org.ow2.asm/asm/jars/asm-5.0.3.jar:/home/nfulton/.ivy2/cache/org.mozilla/rhino/jars/rhino-1.7R4.jar:/home/nfulton/.ivy2/cache/org.mongodb/mongo-java-driver/jars/mongo-java-driver-2.12.4.jar:/home/nfulton/.ivy2/cache/org.mongodb/casbah-query_2.11/jars/casbah-query_2.11-2.7.4.jar:/home/nfulton/.ivy2/cache/org.mongodb/casbah-gridfs_2.11/jars/casbah-gridfs_2.11-2.7.4.jar:/home/nfulton/.ivy2/cache/org.mongodb/casbah-core_2.11/jars/casbah-core_2.11-2.7.4.jar:/home/nfulton/.ivy2/cache/org.mongodb/casbah-commons_2.11/jars/casbah-commons_2.11-2.7.4.jar:/home/nfulton/.ivy2/cache/org.jvnet.mimepull/mimepull/jars/mimepull-1.9.4.jar:/home/nfulton/.ivy2/cache/org.joda/joda-convert/jars/joda-convert-1.2.jar:/home/nfulton/.ivy2/cache/net.sf.jopt-simple/jopt-simple/jars/jopt-simple-4.6.jar:/home/nfulton/.ivy2/cache/joda-time/joda-time/jars/joda-time-2.3.jar:/home/nfulton/.ivy2/cache/javax.mail/mailapi/jars/mailapi-1.4.3.jar:/home/nfulton/.ivy2/cache/javax.activation/activation/jars/activation-1.1.jar:/home/nfulton/.ivy2/cache/io.spray/spray-util_2.11/bundles/spray-util_2.11-1.3.1.jar:/home/nfulton/.ivy2/cache/io.spray/spray-routing_2.11/bundles/spray-routing_2.11-1.3.1.jar:/home/nfulton/.ivy2/cache/io.spray/spray-json_2.11/bundles/spray-json_2.11-1.3.2.jar:/home/nfulton/.ivy2/cache/io.spray/spray-io_2.11/bundles/spray-io_2.11-1.3.1.jar:/home/nfulton/.ivy2/cache/io.spray/spray-httpx_2.11/bundles/spray-httpx_2.11-1.3.1.jar:/home/nfulton/.ivy2/cache/io.spray/spray-http_2.11/bundles/spray-http_2.11-1.3.1.jar:/home/nfulton/.ivy2/cache/io.spray/spray-can_2.11/bundles/spray-can_2.11-1.3.1.jar:/home/nfulton/.ivy2/cache/com.typesafe.slick/slick_2.11/bundles/slick_2.11-2.1.0.jar:/home/nfulton/.ivy2/cache/com.typesafe.slick/slick-codegen_2.11/jars/slick-codegen_2.11-2.1.0.jar:/home/nfulton/.ivy2/cache/com.typesafe.akka/akka-slf4j_2.11/jars/akka-slf4j_2.11-2.3.12.jar:/home/nfulton/.ivy2/cache/com.typesafe.akka/akka-actor_2.11/jars/akka-actor_2.11-2.3.12.jar:/home/nfulton/.ivy2/cache/com.typesafe/config/bundles/config-1.2.1.jar:/home/nfulton/.ivy2/cache/com.googlecode.libphonenumber/libphonenumber/jars/libphonenumber-6.2.jar:/home/nfulton/.ivy2/cache/com.google.guava/guava/bundles/guava-16.0.1.jar:/home/nfulton/.ivy2/cache/com.google.code.findbugs/jsr305/jars/jsr305-3.0.0.jar:/home/nfulton/.ivy2/cache/com.github.nscala-time/nscala-time_2.11/jars/nscala-time_2.11-1.0.0.jar:/home/nfulton/.ivy2/cache/com.github.fge/uri-template/jars/uri-template-0.9.jar:/home/nfulton/.ivy2/cache/com.github.fge/msg-simple/jars/msg-simple-1.1.jar:/home/nfulton/.ivy2/cache/com.github.fge/json-schema-validator/jars/json-schema-validator-2.2.6.jar:/home/nfulton/.ivy2/cache/com.github.fge/json-schema-core/jars/json-schema-core-1.2.5.jar:/home/nfulton/.ivy2/cache/com.github.fge/jackson-coreutils/jars/jackson-coreutils-1.8.jar:/home/nfulton/.ivy2/cache/com.github.fge/btf/jars/btf-1.2.jar:/home/nfulton/.ivy2/cache/com.fasterxml.jackson.core/jackson-databind/jars/jackson-databind-2.2.3.jar:/home/nfulton/.ivy2/cache/com.fasterxml.jackson.core/jackson-core/jars/jackson-core-2.2.3.jar:/home/nfulton/.ivy2/cache/com.fasterxml.jackson.core/jackson-annotations/jars/jackson-annotations-2.2.3.jar:/home/nfulton/.ivy2/cache/com.chuusai/shapeless_2.11/jars/shapeless_2.11-1.2.4.jar:/home/nfulton/.ivy2/cache/ch.qos.logback/logback-core/jars/logback-core-1.0.13.jar:/home/nfulton/.ivy2/cache/ch.qos.logback/logback-classic/jars/logback-classic-1.0.13.jar:/usr/local/Wolfram/Mathematica/10.0/SystemFiles/Links/JLink/JLink.jar:/home/nfulton/local_bin/2016_04_01/lib/idea_rt.jar com.intellij.rt.execution.application.AppMain org.jetbrains.plugins.scala.testingSupport.scalaTest.ScalaTestRunner -s bellerophon.TacticExtractionTests -testName "extractor should extract a proof from the SQLite default database" -showProgressMessages true -C org.jetbrains.plugins.scala.testingSupport.scalaTest.ScalaTestReporter
Testing started at 3:13 PM ...
#
# A fatal error has been detected by the Java Runtime Environment:
#
#  SIGSEGV (0xb) at pc=0x00007fa5866186e0, pid=21470, tid=140348896397056
#
# JRE version: OpenJDK Runtime Environment (7.0_101) (build 1.7.0_101-b00)
# Java VM: OpenJDK 64-Bit Server VM (24.95-b01 mixed mode linux-amd64 compressed oops)
# Derivative: IcedTea 2.6.6
# Distribution: Ubuntu 15.10, package 7u101-2.6.6-0ubuntu0.15.10.1
# Problematic frame:
# C  [libJLinkNativeLibrary.so+0x4436e0]
[error occurred during error reporting (printing problematic frame), id 0xb]

# Failed to write core dump. Core dumps have been disabled. To enable core dumping, try "ulimit -c unlimited" before starting Java again
#
# An error report file with more information is saved as:
# /home/nfulton_unencrypted/KeYmaeraX/hs_err_pid21470.log
[thread 140348888004352 also had an error]

Process finished with exit code 137

Issues with max(R,R)

The max function is not treated as a built-in by the counter-example generator. I don't think QE with max works either.

Static semantics complains about something as well.

QE fails when combining quantifiers and function symbols.

E.g., as in

\forall x (\forall y ((f(x,y)=0 | f(x,y) = 1)))

Lemma application from web ui

Missing base tactics in DerivationInfo

This is a catch-all issue for missing base tactics in DerivationInfo, to be closed only when we have some comprehensive test suite and/or assertions added to the belle data structures.

Known missing:

Identifier 'all' is not recognized as a tactic identifier -- reproduce by extracting tactic from manual proof in ACAS X no delay proof
There are at least three things named DG.

\exists-R dialog formatting bug

Built-in functions not supported in k2m translation for counter-example generation

Due to a k2m conversion problem, I think.

There is an ignored test in BuiltInFunctionSymbolsTests.scala that should be unignored after this is fixed.

Function argument associativity bug

Example:

Functions.
  B Cimpl(R, R, R).
End.
Problem.
  Cimpl(0,1,2) <-> true
End.

produces error message:

2:5 type analysis: Cimpl declared with domain ((Real,Real),Real) but used where domain (Real,(Real,Real)) was expected.
Found:    <unknown> at 2:5 to 2:9
Expected: <unknown>
in 2:5 to 2:9
  B Cimpl(R, R, R).
    ^^^^^

The parser error message isn't misleading; this parses just fine:

Functions.
  B Cimpl(R, R, R).
End.
Problem.
  Cimpl((0,1),2) <-> true
End.

Remove Tactic type annotations

Bug in launcher

From Andre:

Shutting down Mathematica...
...Done
No need to shut down MathKernel if no link has been initialized
No need to shut down MathKernel if no link has been initialized
No need to shut down MathKernel if no link has been initialized
[INFO] [07/26/2016 17:25:31.053] [on-spray-can-akka.actor.default-dispatcher-6] [akka://on-spray-can/user/IO-HTTP/listener-0/0] Message [akka.dispatch.sysmsg.Suspend] from Actor[akka://on-spray-can/user/IO-HTTP/listener-0/0#1022460019] to Actor[akka://on-spray-can/user/IO-HTTP/listener-0/0#1022460019] was not delivered. [2] dead letters encountered. This logging can be turned off or adjusted with configuration settings 'akka.log-dead-letters' and 'akka.log-dead-letters-during-shutdown'.
[INFO] [07/26/2016 17:25:31.054] [on-spray-can-akka.actor.default-dispatcher-6] [akka://on-spray-can/user/IO-HTTP/listener-0/6] Message [akka.dispatch.sysmsg.Suspend] from Actor[akka://on-spray-can/user/IO-HTTP/listener-0/6#780923972] to Actor[akka://on-spray-can/user/IO-HTTP/listener-0/6#780923972] was not delivered. [3] dead letters encountered. This logging can be turned off or adjusted with configuration settings 'akka.log-dead-letters' and 'akka.log-dead-letters-during-shutdown'.
[ERROR] [07/26/2016 17:25:31.055] [on-spray-can-akka.actor.default-dispatcher-6] [akka://on-spray-can/user/IO-HTTP/listener-0] Monitored actor [Actor[akka://on-spray-can/user/hydra#-1613385682]] terminated (akka.actor.DeathPactException)

Exception in thread "main" java.lang.IllegalArgumentException: requirement failed: KeYmaera X Prover 4.2b2

Usage: java -Xss20M -jar keymaerax.jar
  -prove filename -tactic filename [-out filename] |
  -modelplex filename [-out filename] |
  -codegen filename -format C [-vars var1,var2,..,varn] [-out file] |
  -ui [filename] [web server options] |
  -parse [filename] |
  -bparse [filename]

Actions:
  -prove     run KeYmaera X prover on given file with given tactic
  -modelplex synthesize monitor from given file with ModelPlex prover tactic
  -codegen   generate executable code from given file for given target language
  -ui        start web user interface with optional file (if any) and arguments
  -parse     return error code !=0 if the input model file does not parse
  -bparse    return error code !=0 if bellerophon tactic file does not parse

Additional options:
  -mathkernel MathKernel(.exe) path to the Mathematica kernel executable
  -jlink path/to/jlinkNativeLib path to the J/Link native library directory
  -verify   generate and check the final proof certificate (recommended)
  -noverify skip checking proof certificates after proof search
  -interval guard reals by interval arithmetic in floating point (recommended)
  -nointerval  skip interval arithmetic presuming no floating point errors
  -cse      use common subexpression elimination in C code (not recommended)
  -vars     use ordered list of variables, treating others as constant functions
  -kind     ctrl|model kind of monitor to generate
  -lax      enable lax mode with more flexible parser, printer, prover etc.
  -strict   enable strict mode with no flexibility in prover
  -security enable security manager imposing some security restrictions
  -debug    enable debug mode with more exhaustive messages
  -nodebug  disable debug mode to suppress intermediate messages
  -help     Display this usage information
  -license  Show license agreement for using this software

Web server options:
  -tool mathematica|z3

Copyright (c) Carnegie Mellon University.
Use option -license to show the license conditions.

arguments:
        at scala.Predef$.require(Predef.scala:219)
        at edu.cmu.cs.ls.keymaerax.launcher.KeYmaeraX$.main(KeYmaeraX.scala:152)
        at edu.cmu.cs.ls.keymaerax.launcher.KeYmaeraX.main(KeYmaeraX.scala)
…
> Is this just me?
> <ScreenCapture at Tue Jul 26 16:28:56 EDT 2016.png><ScreenCapture at Tue Jul 26 16:28:56 EDT 2016.png>

Mathematica configuration notice blinks on load

It's visible for just a moment while the page is loading even when Mathematica is already configured.

Tactic input should warn when undeclared variables are used.

For example, for the .kyx file

ProgramVariables.
    R x.
End.
Problem.
    x>=0 -> [{x:=x+1;}*]x>=0
End.

the tactic implyR(1) & loop({c>=0}, 1) should give the warning Warning: c is undeclared in the model file. This warning could be shown in the yellow popup thing on the web ui, or even in a modal pop-up.

Bad error message for edge cases during branching tactics

E.g. in the scuba case study (email me for files). Error message:

Core requirement failed: Length of label set (2) should equal number of remaining subgoals (3)

Null point exception in TraceRecordingListener

trace:

2017-08-04 13:46:31 WARN  [on-spray-can-akka.actor.default-dispatcher-17] e.c.c.l.k.h.RestApiActor - Error response details: Tactic failed with error: [Bellerophon Runtime] Unknown throwable thrown during tactic execution
java.lang.NullPointerException: null
	at edu.cmu.cs.ls.keymaerax.tacticsinterface.TraceRecordingListener.end(TraceRecordingListener.scala:102) ~[KeYmaeraX-Web-assembly-4.3.14.jar:4.3.14]
	at edu.cmu.cs.ls.keymaerax.bellerophon.SequentialInterpreter$$anonfun$apply$5.apply(SequentialInterpreter.scala:367) ~[KeYmaeraX-Web-assembly-4.3.14.jar:4.3.14]
	at edu.cmu.cs.ls.keymaerax.bellerophon.SequentialInterpreter$$anonfun$apply$5.apply(SequentialInterpreter.scala:367) ~[KeYmaeraX-Web-assembly-4.3.14.jar:4.3.14]
	at scala.collection.immutable.List.foreach(List.scala:381) ~[KeYmaeraX-Web-assembly-4.3.14.jar:4.3.14]
	at edu.cmu.cs.ls.keymaerax.bellerophon.SequentialInterpreter.apply(SequentialInterpreter.scala:367) ~[KeYmaeraX-Web-assembly-4.3.14.jar:4.3.14]
	at edu.cmu.cs.ls.keymaerax.hydra.BellerophonTacticExecutor$$anon$1.call(BellerophonTacticExecutor.scala:128) ~[KeYmaeraX-Web-assembly-4.3.14.jar:4.3.14]
	at edu.cmu.cs.ls.keymaerax.hydra.BellerophonTacticExecutor$$anon$1.call(BellerophonTacticExecutor.scala:125) ~[KeYmaeraX-Web-assembly-4.3.14.jar:4.3.14]
	at java.util.concurrent.FutureTask.run(FutureTask.java:266) ~[na:1.8.0_91]
	at java.util.concurrent.Executors$RunnableAdapter.call(Executors.java:511) ~[na:1.8.0_91]
	at java.util.concurrent.FutureTask.run(FutureTask.java:266) ~[na:1.8.0_91]
	at java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1142) ~[na:1.8.0_91]
	at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:617) ~[na:1.8.0_91]
	at java.lang.Thread.run(Thread.java:745) ~[na:1.8.0_91]
[ERROR] [08/04/2017 13:46:31.761] [on-spray-can-akka.actor.default-dispatcher-17] [akka.dispatch.Dispatcher] null
java.lang.NullPointerException
	at spray.json.JsonPrinter$class.firstToBeEncoded$1(JsonPrinter.scala:58)

Apparent race condition during boot

The launcher window hangs when my machine is being slow / I have lots going on in the BG. Not sure what's causing that.

ls-lab / keymaerax-release Goto Github PK

keymaerax-release's People

Contributors

Stargazers

Watchers

Forkers

keymaerax-release's Issues

1. Saving Lemmas

2. Using Lemmas

Recommend Projects

Recommend Topics

Recommend Org