add algorithm for fixpoint calculation
This commit is contained in:
parent
8cfbd6116f
commit
ea878975be
2 changed files with 161 additions and 0 deletions
87
lib/util/fixpoint.js
Normal file
87
lib/util/fixpoint.js
Normal file
|
|
@ -0,0 +1,87 @@
|
|||
// Based on:
|
||||
// https://github.com/plug-obp/obp3-algos/blob/1f15cf8c829c7ecd08adb7180aa3c3aefa4f9466/src/main/java/obp3/fixer/Fixer.java
|
||||
// which is in turn based on:
|
||||
// FRANCOIS POTTIER,<a href="https://gallium.inria.fr/~fpottier/publis/fpottier-fix.pdf"> Lazy Least Fixed Points in ML</a>
|
||||
// <a href="https://gitlab.inria.fr/fpottier/fix">OCAML Code</a>
|
||||
|
||||
export const fixer = (eqsFunction, lattice) => {
|
||||
const mFixed = new Map();
|
||||
const mTransient = new Map();
|
||||
const mParents = new Map();
|
||||
|
||||
const mWorkset = []; // Note: we use a Stack (LIFO), but FIFO queue or any other collection would also work.
|
||||
|
||||
let inactive = true;
|
||||
|
||||
const ensureTransient = node => {
|
||||
if (mTransient.has(node)) return;
|
||||
mTransient.set(node, lattice.bottom());
|
||||
mParents.set(node, []);
|
||||
mWorkset.push(node);
|
||||
}
|
||||
|
||||
const solve = current => {
|
||||
if (mFixed.get(current) !== undefined) return;
|
||||
const currentChildren = [];
|
||||
const alive = [true];
|
||||
const requestFunction = node => {
|
||||
if (!alive[0]) throw new Error("must be alive!");
|
||||
const property = mFixed.get(node);
|
||||
if (property !== undefined) return property;
|
||||
ensureTransient(node);
|
||||
currentChildren.push(node);
|
||||
return mTransient.get(node);
|
||||
}
|
||||
const newProperty = eqsFunction(current)(requestFunction);
|
||||
alive[0] = false;
|
||||
|
||||
const isMaximal = lattice.isMaximal(newProperty);
|
||||
if (!isMaximal) {
|
||||
for (const child of currentChildren) {
|
||||
const parents = mParents.get(child);
|
||||
if (parents === undefined) {
|
||||
mParents.set(child, [current]);
|
||||
} else {
|
||||
parents.push(current);
|
||||
}
|
||||
}
|
||||
|
||||
if (!lattice.equality(mTransient.get(current), newProperty)) {
|
||||
mTransient.put(current, newProperty);
|
||||
mWorkset.push(...(mParents.get(current) || []));
|
||||
}
|
||||
}
|
||||
else {
|
||||
mFixed.set(current, newProperty);
|
||||
const oldProperty = mTransient.get(current);
|
||||
mTransient.delete(current);
|
||||
if (!lattice.equality(oldProperty, newProperty)) {
|
||||
mWorkset.push(...(mParents.get(current) || []));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
const get = node => {
|
||||
const property = mFixed.get(node);
|
||||
if (property !== undefined) return property; // return from cache
|
||||
|
||||
if (!inactive) throw new Error("must be inactive!");
|
||||
inactive = false;
|
||||
|
||||
ensureTransient(node);
|
||||
|
||||
while (mWorkset.length > 0) {
|
||||
const current = mWorkset.pop(); // LIFO
|
||||
solve(current);
|
||||
}
|
||||
|
||||
for (const [key, value] of mTransient) {
|
||||
mFixed.set(key, value);
|
||||
}
|
||||
mTransient.clear();
|
||||
inactive = true;
|
||||
return mFixed.get(node);
|
||||
}
|
||||
|
||||
return get;
|
||||
}
|
||||
Loading…
Add table
Add a link
Reference in a new issue