diff --git a/src/InputParser.hs b/src/InputParser.hs
index 3fe89ad..d55d21d 100644
--- a/src/InputParser.hs
+++ b/src/InputParser.hs
@@ -14,6 +14,7 @@ import Processes
 import Linearise
 import Auxiliary
 import Parser
+import ParserAux
 import qualified ParserExpressions
 import qualified ParserExpressionsGlobals
 import DataSpec
@@ -363,7 +364,7 @@ substituteConstantsInProcessTerm functions subs (ActionPrefix reward a aps probs
     where
       expression = (takeWhile (/= '}') (drop 1 (dropWhile (/= '{') a)))
       parsedExpressions_ = ParserExpressionsGlobals.parseExpression expression 1
-      (ParserExpressionsGlobals.Ok parsedExpressions)           = parsedExpressions_
+      (Ok parsedExpressions)           = parsedExpressions_
       newExpressions = [(substituteInExpression subs f,substituteInExpression subs t) | (f,t) <- parsedExpressions]
       aNew_    = (takeWhile (/= '{') a) ++ "{" ++ printExpressions newExpressions ++ "}"	
       aNew     = if elem '{' a then aNew_ else a
@@ -400,7 +401,7 @@ addGlobalToNextStates var (params, c, reward, a, aps, prob, g) | a == "setGlobal
   where
     expression = (takeWhile (/= '}') (drop 1 (dropWhile (/= '{') a)))
     parsedExpressions_ = ParserExpressionsGlobals.parseExpression expression 1
-    (ParserExpressionsGlobals.Ok parsedExpressions__)           = parsedExpressions_
+    (Ok parsedExpressions__)           = parsedExpressions_
     parsedExpressions                                        = [(v,val) | (Variable v,val) <- parsedExpressions__] ++ 
                                                                [(v1++v2,val) | (Function "concat" [Variable v1, Variable v2],val) <- parsedExpressions__]
     newValues = [val | (v,val) <- parsedExpressions, v == var]
diff --git a/src/LPPE.hs b/src/LPPE.hs
index 6dfb7e9..3215877 100644
--- a/src/LPPE.hs
+++ b/src/LPPE.hs
@@ -7,6 +7,7 @@ import Auxiliary
 import Data.List
 import Debug.Trace
 import qualified ParserExpressionsGlobals
+import ParserAux
 import Parser
 
 type PSystem        = (LPPE, InitialState)
@@ -312,7 +313,7 @@ substituteInActionName substitutions action = aNew
   where
       expression = (takeWhile (/= '}') (drop 1 (dropWhile (/= '{') action)))
       parsedExpressions_ = ParserExpressionsGlobals.parseExpression expression 1
-      (ParserExpressionsGlobals.Ok parsedExpressions)           = parsedExpressions_
+      (Ok parsedExpressions)           = parsedExpressions_
       newExpressions = [(substituteInExpression substitutions f,substituteInExpression substitutions t) | (f,t) <- parsedExpressions]
       aNew_    = (takeWhile (/= '{') action) ++ "{" ++ printExpressions newExpressions ++ "}"	
       aNew     = if elem '{' action then aNew_ else action
diff --git a/src/Parser.y b/src/Parser.y
index ed017d3..a0ef8dd 100644
--- a/src/Parser.y
+++ b/src/Parser.y
@@ -1,67 +1,12 @@
 {
 module Parser where
 
+import ParserAux
 import Data.Char
-import Processes
-import Expressions
 import Auxiliary
 import DataSpec
-import Debug.Trace
-
-printExpressions [] = []
-printExpressions updates = infixString [(printExpression var) ++ " := " ++ (printExpression val) | (var,val) <- updates] ", "
-
-data Item = DataActions [(String, ActionType)]
-          | DataHiding [String] 
-          | DataGlobal (Variable, Type) Expression 
-          | DataRenaming [(String, String)] 
-          | DataUntilFormula String
-          | DataFormula Expression
-          | DataEncapsulation [String]   
-          | DataNoCommunication [String]   
-          | DataReach [String]   
-          | DataReachCondition Expression
-          | DataStateReward Expression Expression
-          | DataCommunication [(String, String, String)] 
-          | DataConstant String Expression
-          | DataEnumType String [String] 
-          | DataNat String
-          | DataQueue String
-          | DataRangeType String Expression Expression
-          | DataFunction String [([String], String)]
-          | ParserProcess Process
-          | ParserInitialProcess InitialProcessDefinition
-              deriving (Show, Eq)
-
-data ActionType = None | Bool | IntRange Expression Expression deriving (Show, Eq)
-
-data InitialProcessDefinition = InitSingleProcess InitialProcess
-                              | InitParallel InitialProcessDefinition InitialProcessDefinition
-                              | InitHiding [Action] InitialProcessDefinition
-                              | InitEncapsulation [Action] InitialProcessDefinition
-                              | InitRenaming [(Action, Action)] InitialProcessDefinition
-                                   deriving (Show, Eq)
-
-type LineNumber = Int
-data ParseResult a = Ok a | Failed String
-type ParserMonad a = String -> LineNumber -> ParseResult a
-
-getLineNo :: ParserMonad LineNumber
-getLineNo = \s l -> Ok l
-
-
-thenParserMonad :: ParserMonad a -> (a -> ParserMonad b) -> ParserMonad b
-m `thenParserMonad ` k = \s -> \l ->
-   case (m s l) of 
-       Ok a -> k a s l
-       Failed e -> Failed e
-
-returnParserMonad :: a -> ParserMonad a
-returnParserMonad a = \s -> \l -> Ok a
-
-failParserMonad :: String -> ParserMonad a
-failParserMonad err = \s -> \l -> Failed (err ++ " on line " ++ show l)
-
+import Expressions
+import Processes
 
 }
 
@@ -121,8 +66,11 @@ failParserMonad err = \s -> \l -> Failed (err ++ " on line " ++ show l)
       '='             { TokenEqual }
       '=>'            { TokenImplies }
       '->'            { TokenProbDef }
+      true            { TokenTrue }
+      false           { TokenFalse }
       string          { TokenString $$ }
       hide            { TokenHide }
+      param           { TokenParam }
       rename          { TokenRename }
       bool            { TokenBool }
       actions         { TokenActions }
@@ -150,6 +98,7 @@ Items : {- empty -}             { [] }
       | Item Items              { $1 : $2 }
 
 Item : hide     Strings                                        { DataHiding $2 }
+     | param    Strings                                        { DataParam $2 }
      | rename   StringPairs                                    { DataRenaming $2 }
      | actions  ActionTypes                                    { DataActions $2 }
      | global   string ':' Type '=' Expression                 { DataGlobal ($2, $4) $6 }
@@ -255,7 +204,8 @@ RHS : RHS '++' RHS
     | Expression '=>' RHS                                             { Implication $1 $3 }
     | ProcessInstantiation                                            { $1 }
     | '(' RHS ')'                                                     { $2 }
-    | '<' Expression '>' '.' RHS                                      { LambdaPrefix $2 $5}
+    | '<' Expression '>' '.' RHS                                      { LambdaPrefix (Variable "0") $2 $5}
+    | '<' Expression '>' Reward '.' RHS                               { LambdaPrefix $4 $2 $6}
 
 ProcessInstantiation : string '[' Expressions ']'                     { ProcessInstance $1 (reverse $3) }
                      | string '[' Updates ']'                         { ProcessInstance2 $1 (reverse $3) }
@@ -263,6 +213,8 @@ ProcessInstantiation : string '[' Expressions ']'                     { ProcessI
 
 
 Type         : string                                { TypeName $1 }
+             | Queue                                 { TypeName "Queue" }
+             | Nat                                   { TypeName "Nat" }
              | '{' Expression '..' Expression '}'    { TypeRangeExpressions $2 $4 }
 
 IndepProbs   : IndepProb                        { [$1] }
@@ -347,6 +299,9 @@ data Token = TokenSum
            | TokenDotDot
            | TokenAt
            | TokenHide
+           | TokenParam
+           | TokenTrue
+           | TokenFalse
            | TokenRename
            | TokenEncap
            | TokenAnd
@@ -400,11 +355,14 @@ instance Show Token where
      TokenActions -> "actions"
      TokenComma -> ","
      TokenEqual -> "="
+     TokenTrue -> "true"
+     TokenFalse -> "false"
      TokenNotEqual -> "!="
      TokenNot -> "!"
      TokenPSum -> "psum"
      TokenDotDot -> ".."
      TokenHide -> "hide"
+     TokenParam -> "param"
      TokenGlobal -> "global"
      TokenEncap -> "encap"
      TokenAnd -> "&"
@@ -457,6 +415,25 @@ lexer cont ('h':'i':'d':'e':'\r':cs) = cont TokenHide ('\r':cs)
 lexer cont ('h':'i':'d':'e':'\t':cs) = cont TokenHide ('\t':cs)
 lexer cont ('h':'i':'d':'e':'(':cs) = cont TokenHide ('(':cs)
 
+lexer cont ('p':'a':'r':'a':'m':' ':cs) = cont TokenParam cs
+lexer cont ('p':'a':'r':'a':'m':'\n':cs) = cont TokenParam ('\n':cs)
+lexer cont ('p':'a':'r':'a':'m':'\r':cs) = cont TokenParam ('\r':cs)
+lexer cont ('p':'a':'r':'a':'m':'\t':cs) = cont TokenParam ('\t':cs)
+lexer cont ('p':'a':'r':'a':'m':'(':cs) = cont TokenParam ('(':cs)
+
+lexer cont ('t':'r':'u':'e':' ':cs) = error ("Please use \"T\" instead of \"true\"")
+lexer cont ('t':'r':'u':'e':'\n':cs) = error ("Please use \"T\" instead of \"true\"")
+lexer cont ('t':'r':'u':'e':'\r':cs) = error ("Please use \"T\" instead of \"true\"")
+lexer cont ('t':'r':'u':'e':'\t':cs) = error ("Please use \"T\" instead of \"true\"")
+lexer cont ('t':'r':'u':'e':'(':cs) = error ("Please use \"T\" instead of \"true\"")
+
+lexer cont ('f':'a':'l':'s':'e':' ':cs) = error ("Please use \"F\" instead of \"false\"")
+lexer cont ('f':'a':'l':'s':'e':'\n':cs) = error ("Please use \"F\" instead of \"false\"")
+lexer cont ('f':'a':'l':'s':'e':'\r':cs) = error ("Please use \"F\" instead of \"false\"")
+lexer cont ('f':'a':'l':'s':'e':'\t':cs) = error ("Please use \"F\" instead of \"false\"")
+lexer cont ('f':'a':'l':'s':'e':'(':cs) = error ("Please use \"F\" instead of \"false\"")
+
+
 lexer cont ('g':'l':'o':'b':'a':'l':' ':cs) = cont TokenGlobal cs
 lexer cont ('g':'l':'o':'b':'a':'l':'\n':cs) = cont TokenGlobal ('\n':cs)
 lexer cont ('g':'l':'o':'b':'a':'l':'\r':cs) = cont TokenGlobal ('\r':cs)
@@ -572,7 +549,7 @@ lexNumber cont cs = cont (TokenString var) rest
 
 getString [] = ("","")
 getString ('.':'.':cs) = ("", '.':'.':cs)
-getString (c:cs) | elem c "\n\t\r ',()&=*.<>@+{}^:-!?/|\"[]" = ("", c:cs)
+getString (c:cs) | elem c "\n\t\r ',()&=*.<>@+{}^:-/|\"[]" = ("", c:cs)
                  | otherwise = (str,rest)
   where
     (s,r) = getString cs
diff --git a/src/ParserAux.hs b/src/ParserAux.hs
index a6852e5..d8baaaa 100644
--- a/src/ParserAux.hs
+++ b/src/ParserAux.hs
@@ -1,7 +1,10 @@
 module ParserAux where
 
+import DataSpec
+import Data.Char
 import Expressions
 import Auxiliary
+import Processes
 
 printExpressions [] = []
 printExpressions updates = infixString [(printExpression var) ++ " := " ++ (printExpression val) | (var,val) <- updates] ", "
@@ -57,3 +60,11 @@ returnParserMonad a = \s -> \l -> Ok a
 
 failParserMonad :: String -> ParserMonad a
 failParserMonad err = \s -> \l -> Failed (err ++ " on line " ++ show l)
+
+-- For ParserUntil:
+data UntilFormula     = UntilFormula ActionExpression ActionExpression  deriving (Show, Eq)
+data ActionExpression = ActionName String [String]
+                      | ActionOr   ActionExpression ActionExpression
+                      | ActionNot  ActionExpression
+                      | ActionTrue
+                      deriving (Show, Eq)
diff --git a/src/ParserExpressions.y b/src/ParserExpressions.y
index 964780d..7d98d65 100644
--- a/src/ParserExpressions.y
+++ b/src/ParserExpressions.y
@@ -8,27 +8,7 @@ import Auxiliary
 import DataSpec
 import LPPE
 import Debug.Trace
-
-type LineNumber = Int
-data ParseResult a = Ok a | Failed String
-type ParserMonad a = String -> LineNumber -> ParseResult a
-
-getLineNo :: ParserMonad LineNumber
-getLineNo = \s l -> Ok l
-
-
-thenParserMonad :: ParserMonad a -> (a -> ParserMonad b) -> ParserMonad b
-m `thenParserMonad ` k = \s -> \l ->
-   case (m s l) of 
-       Ok a -> k a s l
-       Failed e -> Failed e
-
-returnParserMonad :: a -> ParserMonad a
-returnParserMonad a = \s -> \l -> Ok a
-
-failParserMonad :: String -> ParserMonad a
-failParserMonad err = \s -> \l -> Failed (err ++ " on line " ++ show l)
-
+import ParserAux
 
 }
 
diff --git a/src/ParserExpressionsGlobals.y b/src/ParserExpressionsGlobals.y
index 9e17b96..8ae81af 100644
--- a/src/ParserExpressionsGlobals.y
+++ b/src/ParserExpressionsGlobals.y
@@ -1,33 +1,12 @@
 {
 module ParserExpressionsGlobals where
 
+import ParserAux
+import DataSpec
 import Data.Char
-import Processes
 import Expressions
 import Auxiliary
-import DataSpec
-import Debug.Trace
-
-type LineNumber = Int
-data ParseResult a = Ok a | Failed String
-type ParserMonad a = String -> LineNumber -> ParseResult a
-
-getLineNo :: ParserMonad LineNumber
-getLineNo = \s l -> Ok l
-
-
-thenParserMonad :: ParserMonad a -> (a -> ParserMonad b) -> ParserMonad b
-m `thenParserMonad ` k = \s -> \l ->
-   case (m s l) of 
-       Ok a -> k a s l
-       Failed e -> Failed e
-
-returnParserMonad :: a -> ParserMonad a
-returnParserMonad a = \s -> \l -> Ok a
-
-failParserMonad :: String -> ParserMonad a
-failParserMonad err = \s -> \l -> Failed (err ++ " on line " ++ show l)
-
+import Processes
 
 }
 
diff --git a/src/ParserUntil.y b/src/ParserUntil.y
index 648236d..4e2ec86 100644
--- a/src/ParserUntil.y
+++ b/src/ParserUntil.y
@@ -4,12 +4,8 @@ module ParserUntil where
 import Data.Char
 import Processes
 
-data UntilFormula     = UntilFormula ActionExpression ActionExpression  deriving (Show, Eq)
-data ActionExpression = ActionName String [String]
-                      | ActionOr   ActionExpression ActionExpression
-                      | ActionNot  ActionExpression
-                      | ActionTrue
-                      deriving (Show, Eq)
+import ParserAux
+
 }
 
 %name parseUntil
diff --git a/src/ToPRISM.hs b/src/ToPRISM.hs
index feefc94..0eff933 100644
--- a/src/ToPRISM.hs
+++ b/src/ToPRISM.hs
@@ -6,6 +6,7 @@ import Data.List
 import Expressions
 import DataSpec
 import ParserUntil
+import ParserAux
 import Processes
 import Simplify
 import Debug.Trace