diff --git a/web/README b/web/README
index 66789901e08b862830efb35731588e8b924a30bd..89a67e71b3350d949900fbeaa0063577e3d36b6a 100644
--- a/web/README
+++ b/web/README
@@ -14,7 +14,7 @@ $ source ../setupenv
** On laraserver **
$ export LD_LIBRARY_PATH=/localhome/leonweb/git/z3/build/
- $ play "run -Dapp.prefix=/leon"
+ $ play "start -Dapp.prefix=/leon"
** Locally **
diff --git a/web/app/controllers/Application.scala b/web/app/controllers/Application.scala
index 94a48eba4f0be87a9d04a0f859bb822b0c78f552..ad0dff194339f1623c62056b8c7fd04f1ec2f072 100644
--- a/web/app/controllers/Application.scala
+++ b/web/app/controllers/Application.scala
@@ -14,10 +14,10 @@ object Application extends Controller {
val examples = VerificationExamples.allExamples ++ SynthesisExamples.allExamples
- def index = Action { implicit request =>
+ def index(powermode : Boolean) = Action { implicit request =>
val prefix = Play.current.configuration.getString("app.prefix").getOrElse("")
- Ok(views.html.index(examples, VerificationExamples.default, prefix))
+ Ok(views.html.index(examples, VerificationExamples.default, prefix, powermode))
}
def getExample(id: Int) = Action {
diff --git a/web/app/models/LeonConsole.scala b/web/app/models/LeonConsole.scala
index 32ba4207e3cd797319cb119fa75f3f99e12956a8..ad3112e7a11c5b4674e8ae053db5481b5bf971f1 100644
--- a/web/app/models/LeonConsole.scala
+++ b/web/app/models/LeonConsole.scala
@@ -35,6 +35,8 @@ object LeonConsole {
(event \ "action").as[String] match {
case "start" =>
session ! Start((event \ "mode").as[String], (event \ "code").as[String])
+ case "startpower" =>
+ session ! StartPower((event \ "flags").asOpt[String].getOrElse(""), (event \ "code").as[String])
case "stop" =>
session ! Stop
case _ =>
@@ -102,7 +104,9 @@ class ConsoleSession extends Actor {
val pipeline = TemporaryInputPhase andThen ExtractionPhase andThen AnalysisPhase
- pipeline.run(ctx)((code, Nil))
+ val analysisResults = pipeline.run(ctx)((code, Nil))
+
+ log(analysisResults.summaryString)
event("stopped")
@@ -123,6 +127,30 @@ class ConsoleSession extends Actor {
error("Invalid request mode: "+mode)
}
+ case StartPower(flags, code) =>
+ val classPath = Play.current.configuration.getString("app.classpath").map(_.split(":").toList).getOrElse(Settings.defaultClassPath())
+
+ event("started")
+ isStarted = true
+
+ log("""> ____ __ __ _ _
+ > __ | _ \ _____ _____ _ __ | \/ | ___ __| | ___ | | __
+ > __ | |_) / _ \ \ /\ / / _ \ '__| | |\/| |/ _ \ / _` |/ _ \ | | __
+ > __ | __/ (_) \ V V / __/ | | | | | (_) | (_| | __/ |_| __
+ > |_| \___/ \_/\_/ \___|_| |_| |_|\___/ \__,_|\___| (_)""".stripMargin('>'))
+
+ var ctx = leon.Main.processOptions(reporter, flags.split(" ").filterNot(_.isEmpty).toList)
+ ctx = ctx.copy(settings = ctx.settings.copy(classPath = classPath))
+
+ val pipeline = TemporaryInputPhase andThen leon.Main.computePipeline(ctx.settings)
+
+ pipeline.run(ctx)((code, Nil)) match {
+ case report: leon.verification.VerificationReport => log(report.summaryString)
+ case report: leon.termination.TerminationReport => log(report.summaryString)
+ case _ =>
+ }
+
+ event("stopped")
case Stop =>
isStarted = false
@@ -140,6 +168,7 @@ object ConsoleProtocol {
case class Start(mode: String, code: String)
+ case class StartPower(flags : String, code : String)
case object Stop
diff --git a/web/app/views/index.scala.html b/web/app/views/index.scala.html
index 39c8d5f6a56e74b95e20baead19ab990b705a839..3bc1aa931dc07f2b8c643a2e6dd42080d4934ac7 100644
--- a/web/app/views/index.scala.html
+++ b/web/app/views/index.scala.html
@@ -1,4 +1,4 @@
-@(exs: List[examples.Example], default: examples.Example, prefix: String)(implicit request: RequestHeader)
+@(exs: List[examples.Example], default: examples.Example, prefix: String, powermode : Boolean)(implicit request: RequestHeader)
@main("Leon Online", prefix) {
<div id="allcontent">
@@ -12,8 +12,13 @@
<div id="leonmain" class="contentbox">
<form id="leoninput" method="POST" action="">
<div id="codecolumn">
- <div id="codebox">@default.code</div>
- <input type="submit" id="askbutton" value="Ask Leon !">
+ <div id="codebox">@default.code</div>
+ <div id="subcodebox">
+ @if(powermode) {
+ <input type="text" id="powerflags" value="--timeout=2" placeholder="add any flags here">
+ }
+ <input type="submit" id="askbutton" value="Run Leon !">
+ </div>
<div><textarea id="consolebox"></textarea></div>
</div>
<div id="selectcolumn">
@@ -51,16 +56,24 @@
}
}
- leonSocket.onmessage = receiveEvent
+ leonSocket.onmessage = receiveEvent;
- var leonStatus = "stopped"
+ var leonStatus = "stopped";
$("#leoninput").submit(function () {
+ $("#consolebox").val("");
+
+ @if(!powermode) {
var msg = JSON.stringify(
{action: "start", mode: $("#leon-mode").val(), code: editor.getValue()}
- )
+ );
+ } else {
+ var msg = JSON.stringify(
+ {action: "startpower", flags: $("#powerflags").val(), code: editor.getValue()}
+ );
+ }
- leonSocket.send(msg)
+ leonSocket.send(msg);
return false;
});
});
diff --git a/web/conf/routes b/web/conf/routes
index 38891796ce33ffa79c2251b73ceef644ce2fc2dc..586dc60cbc3670ad7c977791bb50e9a8071583b2 100644
--- a/web/conf/routes
+++ b/web/conf/routes
@@ -3,7 +3,7 @@
# ~~~~
# Home page
-GET / leon.web.controllers.Application.index
+GET / leon.web.controllers.Application.index(powermode : Boolean ?= false)
GET /ajax/getExample/:id leon.web.controllers.Application.getExample(id: Int)
GET /openConsole leon.web.controllers.Application.openConsole
diff --git a/web/public/stylesheets/leon.css b/web/public/stylesheets/leon.css
index c2c8f7f1966ac1f553ab8a8e947ddc20073bff86..6496e35af0bcf88099e711513eaed6def381d2a7 100644
--- a/web/public/stylesheets/leon.css
+++ b/web/public/stylesheets/leon.css
@@ -130,8 +130,18 @@ li {
margin-bottom: 5px;
}
+#subcodebox {
+ margin: 460px 0px 0px 0px;
+}
+
+#powerflags {
+ margin: 0px 0px 5px 0px;
+ border: 1px solid #666666;
+ width: 700px;
+}
+
#askbutton {
- margin: 460px 0px 5px 0px;
+ margin: 0px 0px 5px 0px;
background-color: transparent;
border: 1px solid #666666;
width: 700px;