Update the example to be the one from the paper.

4 files changed, 45 insertions, 40 deletions

diff --git a/impl/Operator.hpp b/impl/Operator.hpp
index 71a1e68..2c5af75 100644
--- a/impl/Operator.hpp
+++ b/impl/Operator.hpp
@@ -59,10 +59,13 @@ struct Constant : public Operator<T> {
 };
 
 template<typename T>
-struct Increment: public Operator<T> {
+struct Addition: public Operator<T> {
+  Addition(int i) : _value(i) { }
   T operator() (const std::vector< Expression<T>* >& args, const VariableAssignment<T>& ass) const {
-    return (*args[0])(ass) + 1;
+    return (*args[0])(ass) + _value;
   }
+  private:
+  int _value;
 };
 
 #include "VariableAssignment.hpp"
diff --git a/impl/Solver.hpp b/impl/Solver.hpp
deleted file mode 100644
index 11369bc..0000000
--- a/impl/Solver.hpp
+++ /dev/null
@@ -1,17 +0,0 @@
-#ifndef SOLVER_HPP
-#define SOLVER_HPP
-
-#include "Factory.hpp"
-#include "VariableAssignment.hpp"
-
-template<typename T>
-struct Solver {
-  VariableAssignment<T> solveBF(const EquationSystem<T>& system) {
-    VariableAssignment<T> result;
-    for (unsigned int i = 0; i < _var_count; ++i) {
-      result = system(result);
-    }
-  }
-};
-
-#endif
diff --git a/impl/main.cpp b/impl/main.cpp
index 579db25..db3d0f7 100644
--- a/impl/main.cpp
+++ b/impl/main.cpp
@@ -9,41 +9,60 @@
 
 using namespace std;
 
-/*template<typename T>
-struct Complete {
-  Complete(const T& value)
-    : _value(value) { }
-  private:
-  bool _infinity;
-  T _value;
-};*/
-
 typedef std::vector<Expression<float>*> Args;
 typedef Expression<float> E;
 typedef Constant<float> C;
+typedef Addition<float> A;
 typedef Minimum<float> Min;
 
 std::vector< Expression<float>* > empty;
 int main () {
   EquationSystem<float> sys;
   Variable<float>* x = sys.newVariable("x");
+  Variable<float>* y = sys.newVariable("y");
+  Variable<float>* z = sys.newVariable("z");
+
+  Args xPlusArgs;
+  xPlusArgs.push_back(new E(x, empty));
+  Args xMinArgs;
+  xMinArgs.push_back(new E(new A(-1), xPlusArgs));
+  xMinArgs.push_back(new E(y, empty));
+  Args xMaxArgs;
+  xMaxArgs.push_back(new E(new C(0), empty));
+  xMaxArgs.push_back(new E(new Min(), xMinArgs));
+  sys[*x] = sys.newMaxExpression(xMaxArgs);
+  // x = max(0, min(x-1, y))
 
-  Args incArgs;
-  incArgs.push_back(new E(x, empty));
+  Args yPlusArgs;
+  yPlusArgs.push_back(new E(x, empty));
+  Args yMaxArgs;
+  yMaxArgs.push_back(new E(new C(0), empty));
+  yMaxArgs.push_back(new E(new A(5), yPlusArgs));
+  yMaxArgs.push_back(new E(x, empty));
+  sys[*y] = sys.newMaxExpression(yMaxArgs);
+  // y = max(0, x+5, x)
 
-  Args minArgs;
-  minArgs.push_back(new E(new Increment<float>, incArgs));
-  minArgs.push_back(new E(new C(100), empty));
+  Args zPlusArgs1;
+  zPlusArgs1.push_back(new E(z, empty));
+  Args zPlusArgs2;
+  zPlusArgs2.push_back(new E(x, empty));
+  Args zMaxArgs;
+  zMaxArgs.push_back(new E(new C(0), empty));
+  zMaxArgs.push_back(new E(new A(1), zPlusArgs1));
+  zMaxArgs.push_back(new E(new A(0), zPlusArgs2));
+  sys[*z] = sys.newMaxExpression(zMaxArgs);
+  // z = max(0, z+1, x)
 
-  Args maxArgs;
-  maxArgs.push_back(new E(new C(0), empty));
-  maxArgs.push_back(new E(new Min(), minArgs));
 
-  sys[*x] = sys.newMaxExpression(maxArgs);
-  // x = max(0, min(x+1, 100))
 
-  cout << sys.minFixpoint()[*x] << endl;
-  // -> 100, as expected
+  // x = max(0, min(x-1, y))
+  // y = max(0, x+5, x)
+  // z = max(0, z+1, x)
+  // => x: 0, y: 5, z: inf
+  VariableAssignment<float> fixpoint = sys.minFixpoint();
+  cout << "x = " << fixpoint[*x] << endl;
+  cout << "y = " << fixpoint[*y] << endl;
+  cout << "z = " << fixpoint[*z] << endl;
 
   return 0;
 }
diff --git a/impl/output.png b/impl/output.png
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/impl/output.png