ADD test for bdd correctness

pubkey · Nov 30, 2023 · 2bce575 · 2bce575
1 parent 961d9b5
commit 2bce575
Show file tree

Hide file tree

Showing 2 changed files with 43 additions and 15 deletions.
diff --git a/javascript/src/bdd/bdd.generated.ts b/javascript/src/bdd/bdd.generated.ts
@@ -7,7 +7,7 @@ import {
 import type { StateResolveFunctionInput } from '../types/index.js';
 import { stateResolveFunctionByIndex } from '../states/index.js';
 
-export const minimalBddString = '14a1b,c+d2e5f0g/h.i4j*k-l)m(n6oin8pjk8qmc8rmn8snm8tio4umq4vjp4wmr4xns4yeh6zmq6{is6|tx6}mr6~ns6nx6¡en6¢il6£nh6¤in6¥y£/¦z}/§{~/¨|/©uw/ªvw/«an/¬en/bn/®¡n/¯cn/°kn/±¢£/²¤n/³jm/´yk0µac0¶ek0·bc0¸¥k0¹dg0º¡n0»«¯0¼¬°0½c0¾fk0¿®n0À¸n,Á¦r,Â§s,Ã¨s,Ä©r,Åªr,Æ½n,Ç¾k,È¿n,É±k,Ê²n,Ë³m,Ì¾´2Ízu2Î{|2Ï¾º2Ð¹e2ÑÇÀ2ÒÁÄ2ÓÂÃ2Ô¹º2ÕÇÈ2ÖÍm5×Î¤5Øum5Ùvj5ÚÒm5ÛÓÊ5ÜÄm5ÝÅË5ÞÌÑ+ßÖÚ+à×Û+áØÜ+âÙÝ+ãµ»+ä¶¼+å·Æ+æÏÕ+ç¢É+è¤Ê+éjË+êçÐ3ëmã3ìéä3íßã3îàÔ3ïáã3ðâä3ñêì7òíï7óîð7ôçé7õèé7öïå1÷ëå1øñÞ1ùòå1úóæ1û÷ö-ü÷ù-ýøú-þls-ÿôõ-Āln-āmü)Ăÿý)ăĀþ)ĄāĂ9ąmă9ĆĄû*ćąm*Ćć.';
+export const minimalBddString = '14a1b,c+d2e5f0g/h.i4j*k-l)m(n6obh9pce9qnh9rad9scm9tae9uan9vbf9wbe9xbn9ycg9zck9{cn9|nd9}ne9~nf9ng9¡nm9¢nk9£mh9¤mi9¥mj9¦mk9§ml9¨mn9©mc8ª¤{8«¥z8¬¨s8¨n8®mn8¯¨¡8°¨m8±pz7²ª«7³{z7´®7µ}n7¶¤¥7·¨m7¸wo6¹µ}6ºnq6»²¬6¼tu6½wx6¾´¯6¿µn6À®¯6Á¶§6Â·£6Ã¶¨6Ä·¨6Åm¦6Æm¨6Ç¤¥5È¨m5Ém©4Êm®4ËÇ§4ÌÈ£4ÍÇ¬4ÎÃ»4ÏÈ¯4ÐÄ¾4Ñm¦4Òm¯4ÓÆÀ4Ôma3Õmn3ÖÉa3×Ên3ØËr3ÙÁt3ÚÌ|3ÛÂ¹3ÜÍr3ÝÎ¼3ÞÏ|3ßÐ¿3àØÙ2áv¸2ây±2ãÚÛ2ä~º2åµ2æÜÝ2çv½2èy³2éz{2êÞß2ë~n2ìn2íÑÅ2îÒÓ2ï¢n2ðÔb1ñÕn1òÖb1ó×n1ôàá1õâz1öãä1÷æç1øèé1ùêë1úðc0ûñn0üòc0ýón0þmn0ÿÊn0Āôõ0āöå0Ă÷ø0ăùì0Ąíï0ąîï0Ćúû/ćüý/ĈĀā/ĉĂă/ĊÁÂ/ċÃÄ/Čúm.čüm.ĎĆm.ďćm.Đþm.đÿm.ĒĀ§.ēĂ°.ĔĈ§.ĕĉ°.ĖĄ§.ėą°.ĘÁ§.ęÃ¨.ĚĊ§.ěċ¨.ĜÅ§.ĝÆ¨.ĞČč-ğĎď-ĠĐđ-ġĒē-ĢĔĕ-ģĖė-ĤĘę-ĥĚě-ĦĜĝ-ħğĠ,ĨĢģ,ĩĥĦ,ĪĞħ+īġĨ+ĬĤĩ+ĭĪī)ĭĬ(';
 
 let simpleBdd: SimpleBdd | undefined;
 export function getSimpleBdd() {

diff --git a/javascript/src/truth-table-generator/runner.node.ts b/javascript/src/truth-table-generator/runner.node.ts
@@ -6,7 +6,11 @@ import {
     fillTruthTable,
     optimizeBruteForce,
     OptimisationResult,
-    RootNode
+    RootNode,
+    resolveWithSimpleBdd,
+    ResolverFunctions,
+    booleanStringToBoolean,
+    minimalStringToSimpleBdd
 } from 'binary-decision-diagram';
 
 import type { StateActionIdMap } from './types.js';
@@ -33,6 +37,7 @@ import {
     getBetterBdd,
     getQualityOfBdd
 } from './calculate-bdd-quality.js';
+import { orderedStateList } from '../states/index.js';
 
 /**
  * sort object attributes
@@ -48,6 +53,14 @@ export function sortObject<T>(obj: T): T {
         }), {}) as T;
 }
 
+function loadTruthTable() {
+    const truthTable: TruthTable = objectToMap(
+        readJsonFile(OUTPUT_TRUTH_TABLE_PATH)
+    );
+    return truthTable;
+}
+
+
 const unknownValueActionId: number = 42;
 
 async function run() {
@@ -109,11 +122,6 @@ async function run() {
                 let totalAmountOfHandled = 0;
                 let totalAmountOfOptimized = 0;
 
-                function loadTruthTable(): StateActionIdMap {
-                    return objectToMap(
-                        readJsonFile(OUTPUT_TRUTH_TABLE_PATH)
-                    );
-                }
                 let truthTable: StateActionIdMap = loadTruthTable();
                 const startTruthTableEntries = truthTable.size;
 
@@ -213,9 +221,7 @@ async function run() {
         case 'create-bdd':
             (async function createBdd() {
                 console.log('read table..');
-                const truthTable: TruthTable = objectToMap(
-                    readJsonFile(OUTPUT_TRUTH_TABLE_PATH)
-                );
+                const truthTable = loadTruthTable();
                 console.log('table size: ' + truthTable.size);
 
                 // fill missing rows with unknown
@@ -226,6 +232,7 @@ async function run() {
                 );
 
                 console.log('create bdd..');
+
                 const bdd = createBddFromTruthTable(truthTable);
                 console.log('mimizing..');
                 console.log('remove unkown states..');
@@ -248,9 +255,7 @@ async function run() {
             (async function optimizeBdd() {
                 console.log('read table..');
                 let lastBetterFoundTime = new Date().getTime();
-                const truthTable: TruthTable = objectToMap(
-                    readJsonFile(OUTPUT_TRUTH_TABLE_PATH)
-                );
+                const truthTable = loadTruthTable();
                 console.log('table size: ' + truthTable.size);
 
                 // fill missing rows with unknown
@@ -267,6 +272,12 @@ async function run() {
                 console.dir(perfMeasurement);
 
 
+                const resolvers: ResolverFunctions = {};
+                new Array(orderedStateList.length).fill(0).forEach((_x, index) => {
+                    const fn = (state: string) => booleanStringToBoolean((state as any)[index]);
+                    resolvers[index] = fn;
+                });
+
                 function getQuality(bdd: RootNode) {
                     return getQualityOfBdd(
                         bdd,
@@ -280,12 +291,29 @@ async function run() {
                     truthTable,
                     iterations: 10000000,
                     afterBddCreation: (bdd: RootNode) => {
-
                         const lastBetterAgo = new Date().getTime() - lastBetterFoundTime;
                         const lastBetterHours = lastBetterAgo / 1000 / 60 / 60;
                         console.log('Last better bdd found ' + roundToTwoDecimals(lastBetterHours) + 'hours ago');
-
                         bdd.removeIrrelevantLeafNodes(unknownValueActionId);
+
+                        // ensure correctness to have a double-check that the bdd works correctly
+                        const bddMinimalString = bddToMinimalString(bdd);
+                        const simpleBdd = minimalStringToSimpleBdd(bddMinimalString);
+                        for (const [key, value] of loadTruthTable().entries()) {
+                            const bddValue = resolveWithSimpleBdd(
+                                simpleBdd,
+                                resolvers,
+                                key
+                            );
+
+                            if (value !== bddValue) {
+                                console.error('# Error: minimalBdd has different value compared to truth table ' + key);
+                                console.dir({ value, bddValue });
+                                process.exit(-1);
+                            }
+                        }
+
+
                         if (currentBest) {
                             console.log(
                                 'current best bdd has ' + currentBest.countNodes() + ' nodes ' +