Fixed variable showcase in output table

diff --git a/dist/bundle.js b/dist/bundle.js
index 9ed0b35a7460332d6a0869e4d9f53e100ae281db..2c5793ce1d4163e02eee4e2e00a132fb5dfcdf74 100644 (file)
--- a/dist/bundle.js
+++ b/dist/bundle.js
@@ -1 +1 @@
-(()=>{"use strict";class e{constructor(t){let r=e.get_root(t.operators);if(this.root=r[0],this.left=void 0,this.right=void 0,-1==r[1])console.error("Something went wrong during sytax tree creation");else if("Binary"==r[0][0]){let n=t.formula.substring(0,r[1]),i=t.formula.substring(r[1]+1);"("==n.charAt(0)&&(n=n.substring(1,r[1]-1)),"("==i.charAt(0)&&(i=i.substring(1,i.length-1)),this.left=new e(new s(n)),this.right=new e(new s(i))}else if("Unary"==r[0][0]){let r=t.formula.substring(1);"("==r.charAt(0)&&(r=r.substring(1,r.length-1)),this.left=void 0,this.right=new e(new s(r))}}toString(e){let t="";return null==e&&(e=this),null!=e.left&&null!=e.right?t+=`(${e.root[1]}, ${e.left}, ${e.right})`:null!=e.right?t+=`(${e.root[1]}, ${e.right})`:t=e.root[1],t}static get_root(e){if(1==e.length)return[e[0],0];switch(e[0][0]){case"Atom":return[e[1],1];case"Unary":return[e[0],0];case"NestOpen":{let t=0;for(let s=0;s<e.length;s++)if("NestOpen"==e[s][0])t++;else if("NestClose"==e[s][0]&&0==--t)return[e[s+1],s+1]}}return[["Atom",""],-1]}}class t{constructor(e){this.name=e,this.value=!1}setState(e){this.value="0"!=e}}class s{constructor(r){let n=s.is_fbf(r),[i,a,l]=n;this.variables=[];for(let e of l){let s=!1;for(let t of this.variables)t.name==e&&(s=!0);s||this.variables.push(new t(e))}this.formula=r,this.fbf=i,this.operators=a,this.models=[],this.countermodels=[],this.tree=i?new e(this):void 0}evaluate(){let e=[],t="0".repeat(2**this.variables.length);for(let s=0;s<2**this.variables.length;s++){t=s.toString(2).padStart(this.variables.length,"0");for(let e=0;e<t.length;e++)this.variables[e].setState(t[e]);e.push([t,this.evaluateAssignment()])}return e}evaluateAssignment(e){let t=!1;if(null==e&&(e=this.tree),"Atom"==e.root[0])this.variables.forEach((s=>{s.name==e.root[1]&&(t=s.value)}));else if("Unary"==e.root[0])t=!this.evaluateAssignment(e.right);else switch(e.root[1]){case"&":t=this.evaluateAssignment(e.left)&&this.evaluateAssignment(e.right);break;case"|":t=this.evaluateAssignment(e.left)||this.evaluateAssignment(e.right);break;case">":t=!this.evaluateAssignment(e.left)||this.evaluateAssignment(e.right);break;case"-":t=this.evaluateAssignment(e.left)==this.evaluateAssignment(e.right)}return t}static is_fbf(e){let t=[],s=[],r=!1,n=!1;for(let i of e)switch(i){case"!":t.push(["Unary","!"]),r=!0;break;case"&":case"|":case">":case"-":if(r||n)return[!1,[],[]];t.push(["Binary",i]);break;case"(":case"[":case"{":t.push(["NestOpen"]),n=!0;break;case")":case"]":case"}":if(t.push(["NestClose"]),n||r)return[!1,[],[]];break;default:t.push(["Atom",i]),s.push(i),r=!1,n=!1}if(r||n)return[!1,[],[]];let i=Object.assign([],s),a=Object.assign([],t);for(;0!=a.length;)switch(a.pop()[0]){case"Unary":if(void 0===i.pop())return console.error("Unary operation requires one and only one operator"),[!1,[],[]];i.push("_");break;case"Binary":if(void 0===i.pop())return console.error("Binary operation requires exactly 2 operators"),[!1,[],[]];if(void 0===i.pop())return console.error("Binary operation requires exactly 2 operators"),[!1,[],[]];i.push("_");break;case"NestOpen":return console.error("Invalid parentesis"),[!1,[],[]];case"NestClose":{let e=a.reverse().findIndex((e=>"NestOpen"===e[0]));if(-1==e)return console.error("Missing closing parentesis"),[!1,[],[]];a.splice(e,1),a.reverse()}}return 1!=i.length?(console.error("Invalid number of variables"),[!1,[],[]]):[!0,t,s]}}window.checkFormula=function(){let t=document.getElementById("formulaInput").value,r=new s(t.trim());if(r.fbf){document.getElementById("invalidFormula").setAttribute("style","display: none");let t=new e(r),s=document.getElementById("treeString");s.setAttribute("style","display: block"),s.innerHTML=`Syntax tree: </br><b style="padding-left: 20px">${t}</b>`;let n=document.getElementById("formulaTable");n.setAttribute("style","display: block"),n.innerHTML="<h2 class='font-medium leading-tight text-3xl mt-0 mb-2'>Truth table:</h2>"+function(e){let t="<table class='table table-compact'><thead><tr><th>Assignment</th><th>Value</th></tr></thead><tbody>";for(const[s,r]of e)t+=`\n            <tr>\n                <td>${s}</td>\n                <td>${r}</td>\n            </tr>\n        `;return t+="</table>",t}(r.evaluate())}else document.getElementById("invalidFormula").setAttribute("style","display: block")}})();
\ No newline at end of file
+(()=>{"use strict";class e{constructor(t){let r=e.get_root(t.operators);if(this.root=r[0],this.left=void 0,this.right=void 0,-1==r[1])console.error("Something went wrong during sytax tree creation");else if("Binary"==r[0][0]){let a=t.formula.substring(0,r[1]),i=t.formula.substring(r[1]+1);"("==a.charAt(0)&&(a=a.substring(1,r[1]-1)),"("==i.charAt(0)&&(i=i.substring(1,i.length-1)),this.left=new e(new s(a)),this.right=new e(new s(i))}else if("Unary"==r[0][0]){let r=t.formula.substring(1);"("==r.charAt(0)&&(r=r.substring(1,r.length-1)),this.left=void 0,this.right=new e(new s(r))}}toString(e){let t="";return null==e&&(e=this),null!=e.left&&null!=e.right?t+=`(${e.root[1]}, ${e.left}, ${e.right})`:null!=e.right?t+=`(${e.root[1]}, ${e.right})`:t=e.root[1],t}static get_root(e){if(1==e.length)return[e[0],0];switch(e[0][0]){case"Atom":return[e[1],1];case"Unary":return[e[0],0];case"NestOpen":{let t=0;for(let s=0;s<e.length;s++)if("NestOpen"==e[s][0])t++;else if("NestClose"==e[s][0]&&0==--t)return[e[s+1],s+1]}}return[["Atom",""],-1]}}class t{constructor(e){this.name=e,this.value=!1}setState(e){this.value="0"!=e}}class s{constructor(r){let a=s.is_fbf(r),[i,n,l]=a;this.variables=[];for(let e of l){let s=!1;for(let t of this.variables)t.name==e&&(s=!0);s||this.variables.push(new t(e))}this.formula=r,this.fbf=i,this.operators=n,this.models=[],this.countermodels=[],this.tree=i?new e(this):void 0}evaluate(){let e=[],t="0".repeat(2**this.variables.length);for(let s=0;s<2**this.variables.length;s++){t=s.toString(2).padStart(this.variables.length,"0");for(let e=0;e<t.length;e++)this.variables[e].setState(t[e]);e.push([t,this.evaluateAssignment()])}return e}evaluateAssignment(e){let t=!1;if(null==e&&(e=this.tree),"Atom"==e.root[0])this.variables.forEach((s=>{s.name==e.root[1]&&(t=s.value)}));else if("Unary"==e.root[0])t=!this.evaluateAssignment(e.right);else switch(e.root[1]){case"&":t=this.evaluateAssignment(e.left)&&this.evaluateAssignment(e.right);break;case"|":t=this.evaluateAssignment(e.left)||this.evaluateAssignment(e.right);break;case">":t=!this.evaluateAssignment(e.left)||this.evaluateAssignment(e.right);break;case"-":t=this.evaluateAssignment(e.left)==this.evaluateAssignment(e.right)}return t}static is_fbf(e){let t=[],s=[],r=!1,a=!1;for(let i of e)switch(i){case"!":t.push(["Unary","!"]),r=!0;break;case"&":case"|":case">":case"-":if(r||a)return[!1,[],[]];t.push(["Binary",i]);break;case"(":case"[":case"{":t.push(["NestOpen"]),a=!0;break;case")":case"]":case"}":if(t.push(["NestClose"]),a||r)return[!1,[],[]];break;default:t.push(["Atom",i]),s.push(i),r=!1,a=!1}if(r||a)return[!1,[],[]];let i=Object.assign([],s),n=Object.assign([],t);for(;0!=n.length;)switch(n.pop()[0]){case"Unary":if(void 0===i.pop())return console.error("Unary operation requires one and only one operator"),[!1,[],[]];i.push("_");break;case"Binary":if(void 0===i.pop())return console.error("Binary operation requires exactly 2 operators"),[!1,[],[]];if(void 0===i.pop())return console.error("Binary operation requires exactly 2 operators"),[!1,[],[]];i.push("_");break;case"NestOpen":return console.error("Invalid parentesis"),[!1,[],[]];case"NestClose":{let e=n.reverse().findIndex((e=>"NestOpen"===e[0]));if(-1==e)return console.error("Missing closing parentesis"),[!1,[],[]];n.splice(e,1),n.reverse()}}return 1!=i.length?(console.error("Invalid number of variables"),[!1,[],[]]):[!0,t,s]}}window.checkFormula=function(){let e=document.getElementById("formulaInput").value,t=new s(e.trim());if(t.fbf){document.getElementById("invalidFormula").setAttribute("style","display: none");let e=document.getElementById("treeString");e.setAttribute("style","display: block"),e.innerHTML=`Syntax tree: </br><b style="padding-left: 20px">${t.tree}</b>`;let s=document.getElementById("formulaTable");s.setAttribute("style","display: block"),s.innerHTML="<h2 class='font-medium leading-tight text-3xl mt-0 mb-2'>Truth table:</h2>"+function(e,t){let s="<table class='table table-compact'><thead><tr>";for(const t of e)s+=`<th>${t.name}</th>`;s+="<th>Value</th></tr></thead><tbody>";for(const[e,r]of t){s+="<tr>";for(const t of e)s+=`<td>${t}</td>`;s+=`<td>${r}</td>`,s+="</tr>"}return s+="</table>",s}(t.variables,t.evaluate())}else document.getElementById("invalidFormula").setAttribute("style","display: block")}})();
\ No newline at end of file

diff --git a/package-lock.json b/package-lock.json
index de8a1f2320b5b7aba4afbfadb58f3e19128446ed..3adc873e80246227822ee783f17af2a6c281591b 100644 (file)
--- a/package-lock.json
+++ b/package-lock.json
@@ -12,7 +12,7 @@
         "ts-loader": "^9.4.2",
         "typescript": "^4.9.5",
         "webpack": "^5.75.0",
         "ts-loader": "^9.4.2",
         "typescript": "^4.9.5",
         "webpack": "^5.75.0",

-        "webpack-cli": "^5.0.1"
+        "webpack-cli": "^5.1.4"

       }
     },
     "node_modules/@discoveryjs/json-ext": {
       }
     },
     "node_modules/@discoveryjs/json-ext": {


@@ -267,9 +267,9 @@
       }
     },
     "node_modules/@webpack-cli/configtest": {
       }
     },
     "node_modules/@webpack-cli/configtest": {

-      "version": "2.0.1",
-      "resolved": "https://registry.npmjs.org/@webpack-cli/configtest/-/configtest-2.0.1.tgz",
-      "integrity": "sha512-njsdJXJSiS2iNbQVS0eT8A/KPnmyH4pv1APj2K0d1wrZcBLw+yppxOy4CGqa0OxDJkzfL/XELDhD8rocnIwB5A==",
+      "version": "2.1.1",
+      "resolved": "https://registry.npmjs.org/@webpack-cli/configtest/-/configtest-2.1.1.tgz",
+      "integrity": "sha512-wy0mglZpDSiSS0XHrVR+BAdId2+yxPSoJW8fsna3ZpYSlufjvxnP4YbKTCBZnNIcGN4r6ZPXV55X4mYExOfLmw==",

       "dev": true,
       "engines": {
         "node": ">=14.15.0"
       "dev": true,
       "engines": {
         "node": ">=14.15.0"


@@ -280,9 +280,9 @@
       }
     },
     "node_modules/@webpack-cli/info": {
       }
     },
     "node_modules/@webpack-cli/info": {

-      "version": "2.0.1",
-      "resolved": "https://registry.npmjs.org/@webpack-cli/info/-/info-2.0.1.tgz",
-      "integrity": "sha512-fE1UEWTwsAxRhrJNikE7v4EotYflkEhBL7EbajfkPlf6E37/2QshOy/D48Mw8G5XMFlQtS6YV42vtbG9zBpIQA==",
+      "version": "2.0.2",
+      "resolved": "https://registry.npmjs.org/@webpack-cli/info/-/info-2.0.2.tgz",
+      "integrity": "sha512-zLHQdI/Qs1UyT5UBdWNqsARasIA+AaF8t+4u2aS2nEpBQh2mWIVb8qAklq0eUENnC5mOItrIB4LiS9xMtph18A==",

       "dev": true,
       "engines": {
         "node": ">=14.15.0"
       "dev": true,
       "engines": {
         "node": ">=14.15.0"


@@ -293,9 +293,9 @@
       }
     },
     "node_modules/@webpack-cli/serve": {
       }
     },
     "node_modules/@webpack-cli/serve": {

-      "version": "2.0.1",
-      "resolved": "https://registry.npmjs.org/@webpack-cli/serve/-/serve-2.0.1.tgz",
-      "integrity": "sha512-0G7tNyS+yW8TdgHwZKlDWYXFA6OJQnoLCQvYKkQP0Q2X205PSQ6RNUj0M+1OB/9gRQaUZ/ccYfaxd0nhaWKfjw==",
+      "version": "2.0.5",
+      "resolved": "https://registry.npmjs.org/@webpack-cli/serve/-/serve-2.0.5.tgz",
+      "integrity": "sha512-lqaoKnRYBdo1UgDX8uF24AfGMifWK19TxPmM5FHc2vAGxrJ/qtyUyFBWoY1tISZdelsQ5fBcOusifo5o5wSJxQ==",

       "dev": true,
       "engines": {
         "node": ">=14.15.0"
       "dev": true,
       "engines": {
         "node": ">=14.15.0"


@@ -1419,17 +1419,17 @@
       }
     },
     "node_modules/webpack-cli": {
       }
     },
     "node_modules/webpack-cli": {

-      "version": "5.0.1",
-      "resolved": "https://registry.npmjs.org/webpack-cli/-/webpack-cli-5.0.1.tgz",
-      "integrity": "sha512-S3KVAyfwUqr0Mo/ur3NzIp6jnerNpo7GUO6so51mxLi1spqsA17YcMXy0WOIJtBSnj748lthxC6XLbNKh/ZC+A==",
+      "version": "5.1.4",
+      "resolved": "https://registry.npmjs.org/webpack-cli/-/webpack-cli-5.1.4.tgz",
+      "integrity": "sha512-pIDJHIEI9LR0yxHXQ+Qh95k2EvXpWzZ5l+d+jIo+RdSm9MiHfzazIxwwni/p7+x4eJZuvG1AJwgC4TNQ7NRgsg==",

       "dev": true,
       "dependencies": {
         "@discoveryjs/json-ext": "^0.5.0",
       "dev": true,
       "dependencies": {
         "@discoveryjs/json-ext": "^0.5.0",

-        "@webpack-cli/configtest": "^2.0.1",
-        "@webpack-cli/info": "^2.0.1",
-        "@webpack-cli/serve": "^2.0.1",
+        "@webpack-cli/configtest": "^2.1.1",
+        "@webpack-cli/info": "^2.0.2",
+        "@webpack-cli/serve": "^2.0.5",

         "colorette": "^2.0.14",
         "colorette": "^2.0.14",

-        "commander": "^9.4.1",
+        "commander": "^10.0.1",

         "cross-spawn": "^7.0.3",
         "envinfo": "^7.7.3",
         "fastest-levenshtein": "^1.0.12",
         "cross-spawn": "^7.0.3",
         "envinfo": "^7.7.3",
         "fastest-levenshtein": "^1.0.12",


@@ -1464,12 +1464,12 @@
       }
     },
     "node_modules/webpack-cli/node_modules/commander": {
       }
     },
     "node_modules/webpack-cli/node_modules/commander": {

-      "version": "9.5.0",
-      "resolved": "https://registry.npmjs.org/commander/-/commander-9.5.0.tgz",
-      "integrity": "sha512-KRs7WVDKg86PWiuAqhDrAQnTXZKraVcCc6vFdL14qrZ/DcWwuRo7VoiYXalXO7S5GKpqYiVEwCbgFDfxNHKJBQ==",
+      "version": "10.0.1",
+      "resolved": "https://registry.npmjs.org/commander/-/commander-10.0.1.tgz",
+      "integrity": "sha512-y4Mg2tXshplEbSGzx7amzPwKKOCGuoSRP/CjEdwwk0FOGlUbq6lKuoyDZTNZkmxHdJtp54hdfY/JUrdL7Xfdug==",

       "dev": true,
       "engines": {
       "dev": true,
       "engines": {

-        "node": "^12.20.0 || >=14"
+        "node": ">=14"

       }
     },
     "node_modules/webpack-merge": {
       }
     },
     "node_modules/webpack-merge": {


@@ -1763,23 +1763,23 @@
       }
     },
     "@webpack-cli/configtest": {
       }
     },
     "@webpack-cli/configtest": {

-      "version": "2.0.1",
-      "resolved": "https://registry.npmjs.org/@webpack-cli/configtest/-/configtest-2.0.1.tgz",
-      "integrity": "sha512-njsdJXJSiS2iNbQVS0eT8A/KPnmyH4pv1APj2K0d1wrZcBLw+yppxOy4CGqa0OxDJkzfL/XELDhD8rocnIwB5A==",
+      "version": "2.1.1",
+      "resolved": "https://registry.npmjs.org/@webpack-cli/configtest/-/configtest-2.1.1.tgz",
+      "integrity": "sha512-wy0mglZpDSiSS0XHrVR+BAdId2+yxPSoJW8fsna3ZpYSlufjvxnP4YbKTCBZnNIcGN4r6ZPXV55X4mYExOfLmw==",

       "dev": true,
       "requires": {}
     },
     "@webpack-cli/info": {
       "dev": true,
       "requires": {}
     },
     "@webpack-cli/info": {

-      "version": "2.0.1",
-      "resolved": "https://registry.npmjs.org/@webpack-cli/info/-/info-2.0.1.tgz",
-      "integrity": "sha512-fE1UEWTwsAxRhrJNikE7v4EotYflkEhBL7EbajfkPlf6E37/2QshOy/D48Mw8G5XMFlQtS6YV42vtbG9zBpIQA==",
+      "version": "2.0.2",
+      "resolved": "https://registry.npmjs.org/@webpack-cli/info/-/info-2.0.2.tgz",
+      "integrity": "sha512-zLHQdI/Qs1UyT5UBdWNqsARasIA+AaF8t+4u2aS2nEpBQh2mWIVb8qAklq0eUENnC5mOItrIB4LiS9xMtph18A==",

       "dev": true,
       "requires": {}
     },
     "@webpack-cli/serve": {
       "dev": true,
       "requires": {}
     },
     "@webpack-cli/serve": {

-      "version": "2.0.1",
-      "resolved": "https://registry.npmjs.org/@webpack-cli/serve/-/serve-2.0.1.tgz",
-      "integrity": "sha512-0G7tNyS+yW8TdgHwZKlDWYXFA6OJQnoLCQvYKkQP0Q2X205PSQ6RNUj0M+1OB/9gRQaUZ/ccYfaxd0nhaWKfjw==",
+      "version": "2.0.5",
+      "resolved": "https://registry.npmjs.org/@webpack-cli/serve/-/serve-2.0.5.tgz",
+      "integrity": "sha512-lqaoKnRYBdo1UgDX8uF24AfGMifWK19TxPmM5FHc2vAGxrJ/qtyUyFBWoY1tISZdelsQ5fBcOusifo5o5wSJxQ==",

       "dev": true,
       "requires": {}
     },
       "dev": true,
       "requires": {}
     },


@@ -2559,17 +2559,17 @@
       }
     },
     "webpack-cli": {
       }
     },
     "webpack-cli": {

-      "version": "5.0.1",
-      "resolved": "https://registry.npmjs.org/webpack-cli/-/webpack-cli-5.0.1.tgz",
-      "integrity": "sha512-S3KVAyfwUqr0Mo/ur3NzIp6jnerNpo7GUO6so51mxLi1spqsA17YcMXy0WOIJtBSnj748lthxC6XLbNKh/ZC+A==",
+      "version": "5.1.4",
+      "resolved": "https://registry.npmjs.org/webpack-cli/-/webpack-cli-5.1.4.tgz",
+      "integrity": "sha512-pIDJHIEI9LR0yxHXQ+Qh95k2EvXpWzZ5l+d+jIo+RdSm9MiHfzazIxwwni/p7+x4eJZuvG1AJwgC4TNQ7NRgsg==",

       "dev": true,
       "requires": {
         "@discoveryjs/json-ext": "^0.5.0",
       "dev": true,
       "requires": {
         "@discoveryjs/json-ext": "^0.5.0",

-        "@webpack-cli/configtest": "^2.0.1",
-        "@webpack-cli/info": "^2.0.1",
-        "@webpack-cli/serve": "^2.0.1",
+        "@webpack-cli/configtest": "^2.1.1",
+        "@webpack-cli/info": "^2.0.2",
+        "@webpack-cli/serve": "^2.0.5",

         "colorette": "^2.0.14",
         "colorette": "^2.0.14",

-        "commander": "^9.4.1",
+        "commander": "^10.0.1",

         "cross-spawn": "^7.0.3",
         "envinfo": "^7.7.3",
         "fastest-levenshtein": "^1.0.12",
         "cross-spawn": "^7.0.3",
         "envinfo": "^7.7.3",
         "fastest-levenshtein": "^1.0.12",


@@ -2580,9 +2580,9 @@
       },
       "dependencies": {
         "commander": {
       },
       "dependencies": {
         "commander": {

-          "version": "9.5.0",
-          "resolved": "https://registry.npmjs.org/commander/-/commander-9.5.0.tgz",
-          "integrity": "sha512-KRs7WVDKg86PWiuAqhDrAQnTXZKraVcCc6vFdL14qrZ/DcWwuRo7VoiYXalXO7S5GKpqYiVEwCbgFDfxNHKJBQ==",
+          "version": "10.0.1",
+          "resolved": "https://registry.npmjs.org/commander/-/commander-10.0.1.tgz",
+          "integrity": "sha512-y4Mg2tXshplEbSGzx7amzPwKKOCGuoSRP/CjEdwwk0FOGlUbq6lKuoyDZTNZkmxHdJtp54hdfY/JUrdL7Xfdug==",

           "dev": true
         }
       }
           "dev": true
         }
       }

diff --git a/package.json b/package.json
index 9a9fe63fb17a8730e7dc68e72cb9b63f53c955ed..a7f41ee31d58c7073bf7dc8ff8beee73d602f3e2 100644 (file)
--- a/package.json
+++ b/package.json
@@ -13,6 +13,6 @@
     "ts-loader": "^9.4.2",
     "typescript": "^4.9.5",
     "webpack": "^5.75.0",
     "ts-loader": "^9.4.2",
     "typescript": "^4.9.5",
     "webpack": "^5.75.0",

-    "webpack-cli": "^5.0.1"
+    "webpack-cli": "^5.1.4"

   }
 }
   }
 }

diff --git a/src/main.ts b/src/main.ts
index 8bf02b1b206ebe0267105caa9a2e2e4433b7bfda..cf1875c958188d6c0cdbf729d19e14c8936a5aab 100644 (file)
--- a/src/main.ts
+++ b/src/main.ts
@@ -1,35 +1,41 @@
 import { Formula } from "./formula";
 import { Formula } from "./formula";

+import { Atom } from "./atom";

 
 export function checkFormula() {
 
 export function checkFormula() {

-       let input = (document.getElementById("formulaInput") as HTMLInputElement).value;
+    let input = (document.getElementById("formulaInput") as HTMLInputElement).value;

 
 

-       let formula = new Formula(input.trim());
+    let formula = new Formula(input.trim());

 
 

-       if (formula.fbf) {
-               (document.getElementById("invalidFormula") as HTMLElement).setAttribute("style", "display: none");
+    if (formula.fbf) {
+       (document.getElementById("invalidFormula") as HTMLElement).setAttribute("style", "display: none");

 
 

-               let h2 = document.getElementById("treeString") as HTMLElement;
-               h2.setAttribute("style", "display: block");
-               h2.innerHTML = `Syntax tree: </br><b style="padding-left: 20px">${formula.tree}</b>`;
+       let h2 = document.getElementById("treeString") as HTMLElement;
+       h2.setAttribute("style", "display: block");
+       h2.innerHTML = `Syntax tree: </br><b style="padding-left: 20px">${formula.tree}</b>`;

 
 

-               let table = document.getElementById("formulaTable") as HTMLElement;
-               table.setAttribute("style", "display: block");
-               table.innerHTML = "<h2 class='font-medium leading-tight text-3xl mt-0 mb-2'>Truth table:</h2>" + pprint(formula.evaluate());
-       } else {
-               (document.getElementById("invalidFormula") as HTMLElement).setAttribute("style", "display: block");
-       }
+       let table = document.getElementById("formulaTable") as HTMLElement;
+       table.setAttribute("style", "display: block");
+       table.innerHTML = "<h2 class='font-medium leading-tight text-3xl mt-0 mb-2'>Truth table:</h2>" + pprint(formula.variables, formula.evaluate());
+    } else {
+       (document.getElementById("invalidFormula") as HTMLElement).setAttribute("style", "display: block");
+    }

 }
 
 }
 

-function pprint(arr: Array<[string, boolean]>): string {
-       let table = "<table class='table table-compact'><thead><tr><th>Assignment</th><th>Value</th></tr></thead><tbody>";
-       for (const [item, value] of arr) {
-               table += `
-            <tr>
-                <td>${item}</td>
-                <td>${value}</td>
-            </tr>
-        `;
+function pprint(vars: Atom[], arr: Array<[string, boolean]>): string {
+    let table = "<table class='table table-compact'><thead><tr>";
+    for (const atom of vars) {
+       table += `<th>${atom.name}</th>`;
+    }
+    table += "<th>Value</th></tr></thead><tbody>";
+
+    for (const [assignment, value] of arr) {
+       table += "<tr>";
+       for (const bit of assignment) {
+           table += `<td>${bit}</td>`;

        }
        }

-       table += "</table>";
-       return table;
+       table += `<td>${value}</td>`;
+       table += "</tr>";
+    }
+    table += "</table>";
+    return table;

 }
 }