packages feed

smcdel-1.3.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">
<style>
html, body {
  margin: 0;
  height: 100%;
  min-height: 100%;
}
body {
  display: flex;
  flex-direction: column;
  font-family: sans-serif; color:#333;
}
header, footer {
  flex:none;
  padding:0.5em;
  line-height:2;
}
main {
  flex: 1;
  overflow: hidden;
  display: flex;
}
#left, #right {
  flex: 1;
  overflow-y: auto;
  -webkit-overflow-scrolling: touch;
  box-sizing: border-box;
  padding:5px;
  margin:0;
  border:1px solid #666;
}
#smcinput, #output {
  width:100%;
  margin:0px;
  padding:0px;
  height:100%;
  border:none;
  box-sizing:border-box;
}
#output {
  overflow-y:scroll;
}
a {
  color:brown;
  text-decoration:none;
}
a:hover {
  color: #666;
  text-decoration:underline;
}
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;
}
</style>
</head>
<body>
<header>
  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>.
  <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">
    <input type="button" class="expbut" value="CherylsBirthday">
    or enter your own code on the left side, then
    <input id="runbutton" type="submit" value="Run SMCDEL!" onclick="myRequest('check');" title="Run SMCDEL to answer queries - shortcut: Ctrl + s">
    or
    <input id="kripkebutton" type="submit" value="Show model!" onclick="myRequest('knsToKripke');" title="Show the equivalent Kripke model - shortcut: Ctrl + p">
  </div>
</header>
<main>
  <div id="left">
    <div id="smcinput"></div>
  </div>
  <div id="right">
    <div id="output"></div>
  </div>
</main>
<script src="viz-lite.js"></script>
<script src="jquery.js"></script>
<script src="ace.js"></script>
<script src="mode-smcdel.js"></script>
<script src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/3.1.2/es5/tex-mml-chtml.min.js" integrity="sha512-7rZgZU/u5XjLaO7dBpkcvZ2+ilGXbdIak0FXUgMoO+adNy7RUceort055Wn7LkZY3VLwEsSDpi8Ui+32N1vrfw==" crossorigin="anonymous"></script>
<script>
  "use strict";
  var editor = ace.edit("smcinput");
  editor.getSession().setMode("ace/mode/smcdel");
  $(document).ready(function(){
    $('.expbut').click(function() {
      $('#smcinput').val('... loading ...');
      $.get("getExample?filename=" + $(this).val(),
        function(data) {
            editor.getSession().setValue(data);
        });
    });
  });
  function myRequest(url) {
    $.ajax({
      type: "POST",
      url: url,
      data: { "smcinput": editor.getSession().getValue() },
      success:
        function(data,textStatus,jqXHR) {
          $('#output').html(data);
          MathJax.typesetPromise();
        },
      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>
</body>
</html>