diff --git a/src/ModelParser/Lexer.x b/src/ModelParser/Lexer.x
index dfda4b48ea039a644f32996b4325eef2d50114ea..165582da2394548a51b7b2d37a2a295aee7f17b0 100644
--- a/src/ModelParser/Lexer.x
+++ b/src/ModelParser/Lexer.x
@@ -7,6 +7,7 @@ import Numeric
 %wrapper "basic"
  
 $ident = [0-9a-zA-Z!\._]
+$num = [0-9]
 $value = [0-9a-f]
  
 tokens :-
@@ -20,11 +21,13 @@ tokens :-
     "else"      { \s -> Telse}
     "as-array"  { \s -> Tasarray }
     "BitVec"    { \s -> Tbitvec }
+    "Array"     { \s -> Tarray }
     "as"        { \s -> Tas }
     "const"     { \s -> Tconst }
     "true"      { \s -> Tbool True }
     "false"     { \s -> Tbool False }
     "#x"$value+ { \s -> Tvalue (parseHex s) }
+    $num+       { \s -> Tvalue (parseDec s) }
     $ident+     { \s -> Tident s }    
 {
 
@@ -37,6 +40,7 @@ data Token = Tarrow
            | Telse
            | Tasarray
            | Tbitvec
+           | Tarray
            | Tas
            | Tconst
            | Tvalue Int
@@ -47,8 +51,14 @@ data Token = Tarrow
 parseHex :: String -> Int
 parseHex ('#' : 'x' : value) = let [(n, "")] = readHex value in n
 
+parseDec :: String -> Int
+parseDec value = let [(n, "")] = readDec value in n
+
 model1 = "a.null -> false\nj -> #x00000000\ni -> #x00000000\na.length -> #x00000001"
+model1a = model1 ++ "\na -> (_ as-array k!1)"
+model1b = model1 ++ "\na -> ((as const (Array (_ BitVec 32) (_ BitVec 32))) #xffffffff)"
 model2 = "a.length -> #x00000001\na.null -> true\ni!0 -> #x00000000\na -> (_ as-array k!1)\nk!1 -> {\n  #x00000000\n}"
 model3 = "a.length -> #x00000003\ni!0 -> #x00000001\na -> (_ as-array k!1)\nk!1 -> {\n  #x00000002 -> #x00000001\n  #x00000001 -> #x00000000\n  else -> #x00000001\n}"
+model4 = "a.null -> false\nj -> #x00000010\na -> ((as const (Array (_ BitVec 32) (_ BitVec 32))) #xffffffff)\ni -> #x00000000\na.length -> #x00000001"
 
 }
\ No newline at end of file
diff --git a/src/ModelParser/Parser.y b/src/ModelParser/Parser.y
new file mode 100644
index 0000000000000000000000000000000000000000..efa8bd8bee88ea4d1493037a321dbab4653fde4f
--- /dev/null
+++ b/src/ModelParser/Parser.y
@@ -0,0 +1,67 @@
+{
+module ModelParser.Parser where
+
+import ModelParser.Lexer
+}
+
+%name happyParseTokens
+%tokentype { Token }
+%error { parseError }
+%token
+    "->"       { Tarrow }
+    "{"        { Tbopen }
+    "}"        { Tbclose }
+    "("        { Tpopen }
+    ")"        { Tpclose }
+    "_"        { Tunderscore }
+    "else"     { Telse }
+    "as-array" { Tasarray }
+    "BitVec"   { Tbitvec }
+    "Array"    { Tarray }
+    "as"       { Tas }
+    "const"    { Tconst }
+    value      { Tvalue $$ }
+    bool       { Tbool $$ }
+    ident      { Tident $$ }
+%%
+
+Model : ModelList { $1 }
+
+ModelList : ModelEntry ModelList { $1 : $2 }
+          | {- empty -} { [] }
+
+ModelEntry : ident "->" ModelVal { ($1, $3) }
+
+ModelVal : bool { BoolVal $1 }
+         | value { IntVal $1 }
+         | "(" "_" "as-array" ident ")" { ArrayRef $4 }
+         | "(" "(" "as" "const" "(" "Array" "(" "_" "BitVec" value ")" "(" "_" "BitVec" value ")" ")" ")" value ")" { ArrayAsConst $19 }
+         | "{" FuncList "}" { ArrayFunc $2 }
+
+FuncList : FuncEntry FuncList { $1 : $2 }
+         | {- empty -} { [] }
+
+FuncEntry : value "->" value { InstInt $1 $3 }
+          | "else" "->" value { InstElse $3 }
+          | value { InstElse $1 }
+
+{
+data FuncInst = InstInt Int Int
+              | InstElse Int
+              deriving (Show, Read, Eq)
+
+data ModelVal = BoolVal Bool
+              | IntVal Int
+              | ArrayRef String -- TODO: immediately forward to ArrayFunc?
+              | ArrayAsConst Int -- TODO: parse to InstElse?
+              | ArrayFunc [FuncInst]
+              deriving (Show, Read, Eq)
+
+type Model = [(String, ModelVal)]
+
+parseError :: [Token] -> a
+parseError t = error $ "Parse error" ++ show t
+
+parseModel :: String -> Model
+parseModel = happyParseTokens . alexScanTokens
+}
\ No newline at end of file
diff --git a/src/ModelParser/README.md b/src/ModelParser/README.md
new file mode 100644
index 0000000000000000000000000000000000000000..c04389a118a49523d0be99ee24f65f32375f1f07
--- /dev/null
+++ b/src/ModelParser/README.md
@@ -0,0 +1,9 @@
+# ModelParser
+
+To generate the parser and lexer run the following commands from this directory:
+
+```
+cabal install alex happy
+alex Lexer.x
+happy Parser.y
+```
\ No newline at end of file