diff --git a/examples/index.html b/examples/index.html index ac36e5f926b29b90adfe5fd855f9a839938ef4cc..8341e5710c2b598b20cce4358d9c558a341704cd 100644 --- a/examples/index.html +++ b/examples/index.html @@ -35,6 +35,7 @@
  • Sudoku demo
    • +

    About the Reasoner

    diff --git a/examples/minesweeper/minesweeper-js.html b/examples/minesweeper/minesweeper-js.html index e13a9608554bad0f41eb3687ef7441eee55077e6..435118568d15ec01a44a4e8689d204537b419424 100644 --- a/examples/minesweeper/minesweeper-js.html +++ b/examples/minesweeper/minesweeper-js.html @@ -4,6 +4,7 @@ + Limited reasoner demo diff --git a/examples/sudoku/sudoku-js.html b/examples/sudoku/sudoku-js.html index 67adfd9c61cf678d3a4abfe4a750245ac8b19baf..4134b0621b88d3d68725694a47c91a573a9e8edb 100644 --- a/examples/sudoku/sudoku-js.html +++ b/examples/sudoku/sudoku-js.html @@ -4,6 +4,7 @@ + Limited reasoner demo diff --git a/examples/tui/tui-js.html b/examples/tui/tui-js.html index 11ef38167e9cb58e400d4b8b0a0f78ece613535d..4fb2dd42769499444c56e65da85d5411d07d1432 100644 --- a/examples/tui/tui-js.html +++ b/examples/tui/tui-js.html @@ -4,6 +4,7 @@ + Limited reasoner demo @@ -69,6 +70,40 @@ { value: 'test-veggie-with-guarantee', text: 'Test: Veggie 2' }, // { value: 'test-battleship-1x4', text: 'Test: Battleship 1x4' }, // test-battleship-1x4 test is specificially for "my" computer as it assumes a specific "random" ship placement, which is different under Javascript due to different random numbers --> ]; + var help = [ + { value: 'ls', text: 'list predefined examples' }, + { value: 'load ', text: 'load the specified example' }, + { value: '[hide|show]-debug', text: 'show/hide debug output' }, + { value: '', text: '' }, + { value: 'Sort ', text: 'define new sort with specified id' }, + { value: 'Var -> ', text: 'define new variable' }, + { value: 'Name -> ', text: 'define new standard name' }, + { value: 'Fun / -> ', text: 'define new function' }, + { value: '', text: '' }, + { value: 'Let := ', text: 'define formula abbreviation' }, + { value: '', text: '' }, + { value: 'KB: ', text: 'add clausal formula to knowledge base' }, + { value: '', text: '' }, + { value: '', text: 'evaluate query formula in knowledge base ...' }, + { value: 'Query: ', text: '' }, + { value: 'Assert: ', text: '... and fail if formula is false' }, + { value: 'Refute: ', text: '... and fail if formula is true' }, + //t.echo('Formula are of the form:'); + //t.echo(' t == t t /= t literals'); + //t.echo(' ~formula negation'); + //t.echo(' formula v formula disjunction'); + //t.echo(' formula ^ formula conjunction'); + //t.echo(' Ex x formula existential quantification'); + //t.echo(' Fa x formula universal quantification'); + //t.echo(' formula -> formula implication'); + //t.echo(' formula <-> formula implication'); + //t.echo(' K formula knowledge modality, k >= 0'); + //t.echo(' M formula consistency modality, k >= 0'); + //t.echo(' B formula ==> formula conditional belief modality, k, l >= 0'); + //t.echo(' G formula consistency guarantee'); + //t.echo(' ( formula ) brackets'); + //t.echo(' formula-id id of abbreviation'); + ]; @@ -99,6 +134,7 @@ Load an example: + @@ -190,37 +226,18 @@ function loadExample(file) { function lela_exec(command) { var t = $('#terminal').terminal(); if (command == 'help') { + var maxlen = 0; + for (var i = 0; i < help.length; ++i) { + if (maxlen < help[i].value.length) { + maxlen = help[i].value.length; + } + } t.echo('Commands:'); - t.echo(' ls list predefined examples'); - t.echo(' load load the specified example'); - t.echo(' [hide|show]-debug show/hide debug output'); - t.echo(''); - t.echo(' Sort define new sort with specified id'); - t.echo(' Var -> define new variable'); - t.echo(' Name -> define new standard name'); - t.echo(' Fun / -> define new function'); - t.echo(' Let := define formula abbreviation'); - t.echo(' KB: add clausal formula to knowledge base'); - t.echo(' evaluate query formula in knowledge base ...'); - t.echo(' Query: '); - t.echo(' Assert: ... and fail if formula is false'); - t.echo(' Refute: ... and fail if formula is true'); + for (var i = 0; i < help.length; ++i) { + var pad = new Array(maxlen - help[i].value.length + 1).join(' '); + t.echo(' '+ help[i].value + pad +' ' + help[i].text); + } t.echo('See below for the grammar of formulas.'); - //t.echo('Formula are of the form:'); - //t.echo(' t == t t /= t literals'); - //t.echo(' ~formula negation'); - //t.echo(' formula v formula disjunction'); - //t.echo(' formula ^ formula conjunction'); - //t.echo(' Ex x formula existential quantification'); - //t.echo(' Fa x formula universal quantification'); - //t.echo(' formula -> formula implication'); - //t.echo(' formula <-> formula implication'); - //t.echo(' K formula knowledge modality, k >= 0'); - //t.echo(' M formula consistency modality, k >= 0'); - //t.echo(' B formula ==> formula conditional belief modality, k, l >= 0'); - //t.echo(' G formula consistency guarantee'); - //t.echo(' ( formula ) brackets'); - //t.echo(' formula-id id of abbreviation'); } else if (command == 'ls') { var maxlen = 0; for (var i = 0; i < examples.length; ++i) { @@ -249,10 +266,6 @@ $(document).ready(function() { Module.ccall('lela_init', 'void', [], []); - for (var i = 0; i < examples.length; ++i) { - $('#examples').append($('