smcdel-1.1.0: static/index.html
<!DOCTYPE html>
<html lang="en">
<head>
<title>SMCDEL <!-- VERSION NUMBER --></title>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
<meta name="viewport" content="width=device-width, minimum-scale=1.0, maximum-scale=1.0" />
<style type="text/css">
body {
height:100%;
font-family: sans-serif; color:#333;
min-width:500px;
}
a {
color:brown;
text-decoration:none;
}
a:hover {
color: #666;
text-decoration:underline;
}
#left, #right {
float:left;
padding:2px;
margin:2px;
width:48%;
border:1px solid #666;
}
#smcinput, #output {
width:100%;
margin:0px;
padding:0px;
min-height:450px;
height:100%;
border:none;
box-sizing:border-box;
}
#output {
overflow-y:scroll;
}
input[type=button], input[type=submit] {
color:#000;
background-color:#fff;
border:1px solid #666;
border-radius:2px;
}
.expbut {
padding:5px;
margin:0px;
}
#runbutton, #kripkebutton {
font-weight:bold;
padding:3px;
margin:0px;
}
#output svg {
max-width: 100%;
height: auto;
}
.error {
padding:20px;
color:darkred;
}
.footer {
clear:both;
padding-top:1em;
color:#888;
}
.footer a {
color:#888;
}
</style>
</head>
<body>
<p>This is the web interface of <a href="https://github.com/jrclogic/SMCDEL">SMCDEL</a> <!-- VERSION NUMBER -->, a symbolic model checker for <a href="https://plato.stanford.edu/entries/dynamic-epistemic" target="_blank">Dynamic Epistemic Logic</a>.
See <a href="https://homepages.cwi.nl/~jve/papers/16/pdfs/2016-05-23-del-bdd-lori-journal.pdf">this paper</a>
and <a href="https://github.com/jrclogic/SMCDEL/raw/master/SMCDEL.pdf">this technical report</a> for more information.</p>
<div id="menubar">
Load Examples:
<input type="button" class="expbut" value="MuddyChildren" />
<input type="button" class="expbut" value="DrinkingLogicians" />
<input type="button" class="expbut" value="DiningCryptographers" />
or enter your own code on the left side, then
<input id="runbutton" type="submit" value="Run SMCDEL!" onclick="myRequest('check');" title="shortcut: Ctrl + s" />
or
<input id="kripkebutton" type="submit" value="Show Kripke!" onclick="myRequest('knsToKripke');" title="shortcut: Ctrl + p" />
</div>
<div id="left">
<div id="smcinput"></div>
</div>
<div id="right">
<div id="output"></div>
</div>
<script src="viz-lite.js"></script>
<script src="jquery.js"></script>
<script src="ace.js"></script>
<script src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.5/MathJax.js?config=TeX-AMS-MML_HTMLorMML"></script>
<script type="text/x-mathjax-config">
MathJax.Hub.Config({
"HTML-CSS": { linebreaks: { automatic: true } },
SVG: { linebreaks: { automatic: true } }
});
</script>
<script>
"use strict";
var editor = ace.edit("smcinput");
$(document).ready(function(){
$('.expbut').click(function() {
$('#smcinput').val('... loading ...');
$.get("getExample?filename=" + $(this).val(),
function(data) {
editor.getSession().setValue(data);
});
});
});
function myRequest (url) {
$('#output').val('... running ...');
$.ajax({
type: "POST",
url: url,
data: { "smcinput": editor.getSession().getValue() },
success:
function(data,textStatus,jqXHR) {
$('#output').html(data);
MathJax.Hub.Queue(["Typeset",MathJax.Hub]);
},
error:
function(jqXHR,textStatus,errorThrown) {
$('#output').html(jqXHR.responseText);
}
});
}
function toggleLaw() {
$('.lawbdd').fadeToggle();
}
$(document).keydown(function(e) {
if(e.ctrlKey && e.key == "s") {
$("#runbutton").click();
return false;
}
if(e.ctrlKey && e.key == "p") {
$("#kripkebutton").click();
return false;
}
});
</script>
<p class="footer">
Made by <a href="https://malv.in/">Malvin Gattinger</a>.
Using
<a href="https://www.haskell.org/alex/">alex</a>,
<a href="https://www.haskell.org/happy/">happy</a>,
<a href="https://www.haskell.org/">haskell</a>,
<a href="https://mathjax.org/">MathJax</a>,
<a href="https://github.com/scotty-web/scotty">scotty</a>,
<a href="https://www.haskellstack.org/">stack</a>,
and more awesome free software.
</p>
</body>
</html>