1 files changed, 40 insertions, 21 deletions

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;
 }