From fc6be7b80b5dff8e9dda9898fcf7c104da87969c Mon Sep 17 00:00:00 2001
From: Marcell Vazquez-Chanlatte <mvc@linux.com>
Date: Fri, 8 Jul 2016 20:40:53 -0700
Subject: [PATCH] make variables sympy Symbols + more general names

---
 stl.py        | 2 +-
 stl_parser.py | 8 +++++---
 2 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/stl.py b/stl.py
index 553a6c8..3537585 100644
--- a/stl.py
+++ b/stl.py
@@ -31,7 +31,7 @@ class LinEq(namedtuple("LinEquality", ["terms", "op", "const"])):
 class Var(namedtuple("Var", ["kind", "id", "time"])):
     def __repr__(self):
         time_str = "[{}]".format(self.time)
-        return "{k}{i}{t}".format(k=self.kind.name, i=self.id, t=time_str)
+        return "{i}{t}".format(k=self.kind.name, i=self.id, t=time_str)
 
 
 class Term(namedtuple("Term", ["coeff", "var"])):
diff --git a/stl_parser.py b/stl_parser.py
index c02cf10..28fc5a0 100644
--- a/stl_parser.py
+++ b/stl_parser.py
@@ -22,6 +22,8 @@ from funcy import flatten
 import numpy as np
 from lenses import lens
 
+from sympy import Symbol
+
 from stl import stl
 
 STL_GRAMMAR = Grammar(u'''
@@ -54,7 +56,7 @@ prime = "'"
 pm = "+" / "-"
 dt = "dt"
 unbound = "?"
-id = ("x" / "u" / "w") ~r"\d+" 
+id = ("x" / "u" / "w") ~r"[a-zA-z\d]*" 
 const = ~r"[\+\-]?\d*(\.\d+)?"
 op = ">=" / "<=" / "<" / ">" / "="
 _ = ~r"\s"+
@@ -109,8 +111,8 @@ class STLVisitor(NodeVisitor):
     visit_and = partialmethod(binop_visitor, op=stl.And)
 
     def visit_id(self, name, _):
-        var_kind, *iden = name.text
-        return stl.str_to_varkind[var_kind] ,int("".join(iden))
+        var_kind, *_ = name.text
+        return stl.str_to_varkind[var_kind] , Symbol(name.text)
 
     def visit_var(self, _, children):
         (var_kind, iden), time_node = children