1 files changed, 26 insertions, 16 deletions

diff --git a/impl/main.cpp b/impl/main.cpp
index c5a0be6..0082686 100644
--- a/impl/main.cpp
+++ b/impl/main.cpp
@@ -9,6 +9,7 @@
 #include "Expression.hpp"
 #include "MaxStrategy.hpp"
 #include "EquationSystem.hpp"
+#include "Complete.hpp"
 
 extern "C" {
 #include "EquationSystemParser.h"
@@ -17,12 +18,6 @@ extern "C" {
 
 using namespace std;
 
-typedef std::vector<Expression<float>*> Args;
-typedef Expression<float> E;
-typedef Constant<float> C;
-typedef Addition<float> A;
-typedef Minimum<float> Min;
-
 template<typename T>
 Expression<T>* treeToExpression(pANTLR3_BASE_TREE node, EquationSystem<T>& system) {
   ANTLR3_UINT32 num = node->getChildCount(node);
@@ -31,12 +26,16 @@ Expression<T>* treeToExpression(pANTLR3_BASE_TREE node, EquationSystem<T>& syste
 
   // leaf node - constant or variable
   if (num == 0) {
-    stringstream stream(name);
-    T output;
-    if (stream >> output) {
-      return system.newExpression(new Constant<T>(output), vector<Expression<T>*>());
+    if (name == "inf") {
+      return system.newExpression(new Constant<T>(infinity<T>()), vector<Expression<T>*>());
     } else {
-      return system.newExpression(system.newVariable(name), vector<Expression<T>*>());
+      stringstream stream(name);
+      T output;
+      if (stream >> output) {
+        return system.newExpression(new Constant<T>(output), vector<Expression<T>*>());
+      } else {
+        return system.newExpression(system.newVariable(name), vector<Expression<T>*>());
+      }
     }
   }
 
@@ -58,6 +57,13 @@ Expression<T>* treeToExpression(pANTLR3_BASE_TREE node, EquationSystem<T>& syste
       op = new Addition<T>();
     } else if (name == "-") {
       op = new Subtraction<T>();
+    } else if (name == ";") {
+      op = new Comma<T>();
+    } else if (name == "GUARD") {
+      op = new Guard<T>();
+    } else {
+      std::cerr << "Unknown leaf node type: " << name << std::endl;
+      throw "Unknown leaf node type";
     }
     return system.newExpression(op, args);
   }
@@ -83,7 +89,7 @@ void treeToSystem(pANTLR3_BASE_TREE node, EquationSystem<T>& system) {
   }
 }
 
-std::vector< Expression<float>* > empty;
+typedef Complete<int> ZBar;
 int main (int argc, char* argv[]) {
   pANTLR3_INPUT_STREAM input;
   pEquationSystemLexer lex;
@@ -97,12 +103,16 @@ int main (int argc, char* argv[]) {
 
   EquationSystemParser_equation_system_return ret = parser -> equation_system(parser);
 
-  EquationSystem<float> system;
-  treeToSystem<float>(ret.tree, system);
+  EquationSystem<ZBar> system;
+  treeToSystem<ZBar>(ret.tree, system);
   // DO MORE HERE
 
-  VariableAssignment<float> rho = system.minFixpoint();
-  const std::vector<Variable<float>*> vars = system.vars();
+  VariableAssignment<ZBar> rho = system.minFixpoint(NaiveFixpoint<ZBar>());
+  std::cout << rho << std::endl;
+  rho = system.minFixpoint(RecursiveFixpoint<ZBar>());
+  std::cout << rho << std::endl;
+
+  const std::vector<Variable<ZBar>*> vars = system.vars();
   for (unsigned int i = 0, size = vars.size(); i < size; ++i) {
     cout << vars[i]->name() << " = " << rho[*vars[i]] << endl;
   }