diff --git a/HACKING b/HACKING
index 48495a128c0de336c4f0c73e703c290f09876431..c76163313a1e2065fa8a16d86ab30d29ff53083f 100644
--- a/HACKING
+++ b/HACKING
@@ -15,15 +15,18 @@ assumption must hold that negations are only in front of atomic propositions
 its dual, as we convert to NNF later. For example:
 
   | CONST of string (* constant functor with value string *)
+  | CONSTN of string (* constant functor with value string *)
 
 Do the analogous thing for the type hcFormula_node in the same files!
 
-  | HCONST of string (* constant functor w
+  | HCONST of string (* constant functor w *)
+  | HCONSTN of string (* constant functor w *)
 
 Recall: edit both the ml and the mli-file. Do the analogous thing for
 formulaType in CoAlgMisc.mli and CoAlgMisc.ml:
 
   | ConstF (* constant functor *)
+  | ConstnF (* constant functor *)
 
 If you build now, you will see alot of warnings concerning non-exhaustive
 pattern matchings. We will fix them later.
@@ -53,6 +56,10 @@ And then rebuild with:
 
   ocaml setup.ml -build
 
+You have to extend the parsing in the parse_rest function in CoAlgFormula.ml. If
+you introduce another symbol that was not used before, you have to extend the
+global variable lexer in CoAlgFormula.ml accordingly.
+
 These contain:
 
   - detClosure: Check that a formula has the correct sort and call detClosure if
@@ -66,6 +73,10 @@ These contain:
       if func <> Constant || List.length sortlst <> 1
       then raise (C.CoAlgException "=-formula is used in wrong sort.")
       else ();
+    | C.HCCONSTN _ ->
+      if func <> Constant || List.length sortlst <> 1
+        then raise (C.CoAlgException "=-formula is used in wrong sort.")
+        else ();
 
   - in initTables: Destruct the algebraic datatype into its parts. 
 
@@ -77,7 +88,10 @@ These contain:
     subformulars of formula.
 
   - convert_post -- totally analogous to iter.
-
   - nnfNeg -- return the negated formula in nnf.
+  - nnf -- return the formula in nnf.
+  - simplify -- simplifiy the formula
+  - And other utility functions: equal_hcFormula_node, equal_hcFormula_node,
+    hash_hcFormula_node, toFml_hcFormula_node, negNde_hcFormula_node, hc_formula
 
 // vim: tw=80 ft=asciidoc
diff --git a/INSTALL b/INSTALL
index 445621ac177cfc68741e65f9172785b9892bc290..3fc2ac6affd971a2cd3e5132dc136b9745427d38 100644
--- a/INSTALL
+++ b/INSTALL
@@ -42,11 +42,17 @@ In case there is no setup.ml yet, create it with oasis:
 
     oasis setup
 
+
+In particular, if you have cloned cool via git, then you will need
+to create setup.ml using the command above.
+
 Then compile it:
 
     ocaml setup.ml -configure
     ocaml setup.ml -build
 
+(There will be some warnings.)
+
 Now you have a freshly built coalg.native in the toplevel directory.
 
 If you want the executables statically linked, then run the configure step with
@@ -88,6 +94,9 @@ To see a longer list of example formulas, just run the testsuite:
 
   ./cool-testsuite.native
 
+(Note: The tests for GML and PML will fail due to a version change
+in the GNU LPK library.)
+
 Coalition Logic
 ~~~~~~~~~~~~~~~
 Some formulas are
diff --git a/_oasis b/_oasis
index 8fb6893fa04a404b33441fccefcc4b43808f4b78..b114ffaa724aa3800bb9f44d0868192324f447ff 100644
--- a/_oasis
+++ b/_oasis
@@ -1,4 +1,4 @@
-OASISFormat:    0.4
+OASISFormat:    0.3
 Name:           cool
 Version:        0.1
 Synopsis:       Coalgebraic Ontology Logic solver
diff --git a/src/coalg/coalg.ml b/src/coalg/coalg.ml
index f6c650695593e3e266a1ca0a252d94930aa4930b..33322cee4b6be7177fb054728a399402b6dda35d 100644
--- a/src/coalg/coalg.ml
+++ b/src/coalg/coalg.ml
@@ -45,6 +45,7 @@ let printUsage () =
   print_endline "       <functor> in { MultiModalK (or equivalently K)";
   print_endline "                      MultiModalKD (or equivalently KD)";
   print_endline "                      CoalitionLogic (or equivalently CL)";
+  print_endline "                      Const (or equivalently Constant)";
   print_endline "                      PML";
   print_endline "                      GML";
   print_endline "                    }";
diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index 607e93acfe28577e4e577b17b8aca7a1f75f27f7..3e10e9e43090e87d2035b9110b14099b49a2cae4 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -51,6 +51,8 @@ type formula =
                                       (*  probability of at least 50% *) 
   | LESSPROBFAIL of rational * formula (* = [1/2] C = {< 1/2} ¬ C ---> C fails with *)
                                         (* probability of less than 50% *)
+  | CONST of string  (* constant functor with value string *)
+  | CONSTN of string  (* constant functor with value other than string *)
   | CHC of formula * formula
   | CHCN of formula * formula
   | FUS of bool * formula
@@ -95,6 +97,8 @@ let rec sizeFormula f =
   | LESSPROBFAIL (_, f1)
   | MORETHAN (_, _, f1)
   | MAXEXCEPT (_, _, f1) -> succ (sizeFormula f1)
+  | CONST _
+  | CONSTN _ -> 1
   | CHC (f1, f2)
   | CHCN (f1, f2) -> succ (sizeFormula f1 + sizeFormula f2)
   | FUS (_, f1) -> succ (sizeFormula f1)
@@ -106,11 +110,15 @@ let rec sizeFormula f =
 let sizeSortedFormula f = sizeFormula (snd f)
 
 
+(* think of func: (formula -> unit) -> formula -> unit as identity.
+  iterate over all subformulae and collect side effects. *)
 let rec iter func formula =
     func formula;
     let proc = iter func in (* proc = "process" *)
     match formula with
     | TRUE | FALSE | AP _ -> ()
+    | CONST _
+    | CONSTN _ -> ()
     | NOT a | AT (_,a)
     | EX (_,a) | AX (_,a) -> proc a
     | OR (a,b) | AND (a,b)
@@ -128,6 +136,8 @@ let rec convert_post func formula = (* run over all subformulas in post order *)
   let formula = (match formula with
   (* 0-ary constructors *)
   | TRUE | FALSE | AP _ -> formula
+  | CONST _
+  | CONSTN _ -> formula
   (* unary *)
   | NOT a -> NOT (c a)
   | AT (s,a) -> AT (s,c a)
@@ -308,6 +318,10 @@ let rec exportFormula_buffer sb f =
       Buffer.add_string sb " + ";
       exportFormula_buffer sb f2;
       Buffer.add_string sb ")"
+  | CONST s -> Buffer.add_string sb "=";
+      Buffer.add_string sb s
+  | CONSTN s -> Buffer.add_string sb "~=";
+      Buffer.add_string sb s
   | CHCN (f1, f2) ->
       Buffer.add_string sb "~(";
       exportFormula_buffer sb (negate f1);
@@ -394,6 +408,8 @@ let rec exportTatlFormula_buffer sb f =
   | MORETHAN _
   | MAXEXCEPT _
   | AT _
+  | CONST _
+  | CONSTN _
   | CHC _
   | CHCN _
   | ATLEASTPROB _
@@ -469,7 +485,7 @@ let exportQueryParsable tbox (_,f) =
 
 let lexer = A.make_lexer 
     [":";";";"|-";"(";")";"=>";"<=>";"|";"&";"~";"@";"True";"False";"<";">";"[";"]";"{<=";"{>=";"}";"+";"[pi1]";"[pi2]"
-    ;"[{";"}]";"<{";"}>";",";"/";"{<"
+    ;"[{";"}]";"<{";"}>";",";"/";"{<";"="
     ] 
 
 let mk_exn s = CoAlgException s
@@ -638,6 +654,13 @@ and parse_rest ts =
       if (denom <> 0)
       then LESSPROBFAIL (rational_of_int n denom, NOT f1)
       else A.printError mk_exn ~ts "The \"Less than\" < is not implemented yet"
+  | A.Kwd "=" -> begin
+          match Stream.next ts with
+          (* | A.Int s *)
+          | A.Kwd s
+          | A.Ident s -> CONST s
+          | _ -> A.printError mk_exn ~ts "constant = expects an identifier afterwards"
+    end
   | A.Kwd "(" -> begin
       let f = parse_formula ts in
       match Stream.next ts with
@@ -785,6 +808,8 @@ let rec nnfNeg f =
   | MAXEXCEPT (n, s, f1) -> MORETHAN (n, s, nnfNeg f1)
   | ATLEASTPROB (p, f1) -> LESSPROBFAIL (p, nnfNeg f1)
   | LESSPROBFAIL (p, f1) -> ATLEASTPROB (p, nnfNeg f1)
+  | CONST s -> CONSTN s
+  | CONSTN s -> CONST s
   | CHC (f1, f2) -> CHCN (nnfNeg f1, nnfNeg f2)  
   | CHCN (f1, f2) -> CHC (nnfNeg f1, nnfNeg f2)  
   | FUS (first, f1) -> FUS (first, nnfNeg f1)
@@ -801,7 +826,9 @@ and nnf f =
   | TRUE
   | FALSE
   | AP _
-  | NOT (AP _) -> f
+  | NOT (AP _)
+  | CONST _
+  | CONSTN _ -> f
   | NOT f1 -> nnfNeg f1
   | AT (s, f1) ->
       let ft1 = nnf f1 in
@@ -980,6 +1007,8 @@ let rec simplify f =
   | ATLEASTPROB (p,f1) ->
       let ft1 = simplify f1 in
       if (ft1 == f1) then f else ATLEASTPROB (p,ft1)
+  | CONST _
+  | CONSTN _ -> f (* no simplifications possible *)
   | CHC (f1, f2) ->
       let ft1 = simplify f1 in
       let ft2 = simplify f2 in
@@ -1446,6 +1475,8 @@ and hcFormula_node =
   | HCMAXEXCEPT of int * string * hcFormula (* GML Box *)
   | HCATLEASTPROB of rational * hcFormula
   | HCLESSPROBFAIL of rational * hcFormula
+  | HCCONST of string
+  | HCCONSTN of string
   | HCCHC of hcFormula * hcFormula
   | HCCHCN of hcFormula * hcFormula
   | HCFUS of bool * hcFormula
@@ -1459,6 +1490,8 @@ let equal_hcFormula_node f1 f2 =
   match f1, f2 with
   | HCTRUE, HCTRUE -> true
   | HCFALSE, HCFALSE -> true
+  | HCCONST s1, HCCONST s2
+  | HCCONSTN s1, HCCONSTN s2
   | HCAP s1, HCAP s2
   | HCNOT s1, HCNOT s2 -> compare s1 s2 = 0
   | HCAT (s1, f1), HCAT (s2, f2) -> compare s1 s2 = 0 && f1 == f2
@@ -1496,6 +1529,8 @@ let equal_hcFormula_node f1 f2 =
   | HCMAXEXCEPT _, _
   | HCATLEASTPROB _, _
   | HCLESSPROBFAIL _, _
+  | HCCONST _, _
+  | HCCONSTN _, _
   | HCCHC _, _
   | HCCHCN _, _
   | HCFUS _, _ -> false
@@ -1524,6 +1559,8 @@ let hash_hcFormula_node f =
   | HCFUS (first, f1) -> 19 * (19 * (Hashtbl.hash first) + f1.HC.hkey) + 13
   | HCENFORCES (s, f1) -> 19 * (19 * (Hashtbl.hash s) + f1.HC.hkey) + 14
   | HCALLOWS   (s, f1) -> 19 * (19 * (Hashtbl.hash s) + f1.HC.hkey) + 15
+  | HCCONST s -> Hashtbl.hash s + 16
+  | HCCONSTN s -> Hashtbl.hash s + 17
 
 (** Determines the "real" formula of a formula node.
     @param f A formula node.
@@ -1546,6 +1583,8 @@ let toFml_hcFormula_node f =
   | HCMAXEXCEPT (n, s, f1) -> MAXEXCEPT (n, s, f1.HC.fml)
   | HCATLEASTPROB (p, f1) -> ATLEASTPROB (p, f1.HC.fml)
   | HCLESSPROBFAIL (p, f1) -> LESSPROBFAIL (p, f1.HC.fml)
+  | HCCONST s -> CONST s
+  | HCCONSTN s -> CONSTN s
   | HCCHC (f1, f2) -> CHC (f1.HC.fml, f2.HC.fml)
   | HCCHCN (f1, f2) -> CHCN (f1.HC.fml, f2.HC.fml)
   | HCFUS (first, f1) -> FUS (first, f1.HC.fml)
@@ -1571,6 +1610,8 @@ let negNde_hcFormula_node f =
   | HCMAXEXCEPT (n, s, f1) -> HCMORETHAN (n, s, f1.HC.neg)
   | HCATLEASTPROB (p, f1) -> HCLESSPROBFAIL (p, f1.HC.neg)
   | HCLESSPROBFAIL (p, f1) -> HCATLEASTPROB (p, f1.HC.neg)
+  | HCCONST s -> HCCONSTN s
+  | HCCONSTN s -> HCCONST s
   | HCCHC (f1, f2) -> HCCHCN (f1.HC.neg, f2.HC.neg)
   | HCCHCN (f1, f2) -> HCCHC (f1.HC.neg, f2.HC.neg)
   | HCFUS (first, f1) -> HCFUS (first, f1.HC.neg)
@@ -1638,6 +1679,10 @@ let rec hc_formula hcF f =
       HcFormula.hashcons hcF (HCATLEASTPROB (p, hc_formula hcF f1))
   | LESSPROBFAIL (p, f1) ->
       HcFormula.hashcons hcF (HCLESSPROBFAIL (p, hc_formula hcF f1))
+  | CONST s ->
+      HcFormula.hashcons hcF (HCCONST s)
+  | CONSTN s ->
+      HcFormula.hashcons hcF (HCCONSTN s)
   | CHC (f1, f2) ->
       let tf1 = hc_formula hcF f1 in
       let tf2 = hc_formula hcF f2 in
diff --git a/src/lib/CoAlgFormula.mli b/src/lib/CoAlgFormula.mli
index 7e59944f248eaadcb63bca433ab60dc3994cd97e..74bb2e066dcd9f1f97ad6feaed828d157edc9663 100644
--- a/src/lib/CoAlgFormula.mli
+++ b/src/lib/CoAlgFormula.mli
@@ -33,7 +33,9 @@ type formula =
   | ATLEASTPROB of rational * formula (* = {>= 1/2} C  ---> C occurs with *)
                                       (*  probability of at least 50% *) 
   | LESSPROBFAIL of rational * formula (* = [1/2] C = {< 1/2} ¬ C ---> C fails with *)
-                                        (* probability of less than 50% *)
+                                       (* probability of less than 50% *)
+  | CONST of string  (* constant functor with value string *)
+  | CONSTN of string  (* constant functor with value other than string *)
   | CHC of formula * formula
   | CHCN of formula * formula
   | FUS of bool * formula
@@ -135,6 +137,8 @@ and hcFormula_node =
   | HCMAXEXCEPT of int * string * hcFormula (* GML Box *)
   | HCATLEASTPROB of rational * hcFormula
   | HCLESSPROBFAIL of rational * hcFormula (* the probability for failing is less than ... *)
+  | HCCONST of string
+  | HCCONSTN of string
   | HCCHC of hcFormula * hcFormula
   | HCCHCN of hcFormula * hcFormula
   | HCFUS of bool * hcFormula
diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml
index f24836f1f8d0d0c9154bc9b70e7ebec718befdb1..bd7093d1b7d8a53e0a6ec86fb503990ad68ece2b 100644
--- a/src/lib/CoAlgMisc.ml
+++ b/src/lib/CoAlgMisc.ml
@@ -71,6 +71,7 @@ type functors =
   | CoalitionLogic
   | GML
   | PML
+  | Constant
   | Choice
   | Fusion
 
@@ -83,6 +84,8 @@ let unaryfunctor2name : (functors*string) list =
   ; (MultiModalK , "K")
   ; (MultiModalKD , "KD")
   ; (CoalitionLogic , "CL")
+  ; (Constant , "Const")
+  ; (Constant , "Constant")
   ]
 
 let functor2name : (functors*string) list =
@@ -125,6 +128,8 @@ type formulaType =
   | MaxExceptF(* at most n exceptions = box in gml *)
   | AtLeastProbF (* for PML *)
   | LessProbFailF (* box for PML *)
+  | ConstF (* constant functor *)
+  | ConstnF (* constant functor *)
   | ChcF (* Choice *)
   | FusF (* Fusion *)
 
@@ -683,6 +688,15 @@ let rec detClosure nomTbl hcF fset atset nomset s f =
             TODO: add ¬ f1 to the closure!
         detClosure nomTbl hcF fset atset nomset (List.hd sortlst) (f1.HC.node.negNde)
         *)
+    | C.HCCONST _ ->
+      if func <> Constant || List.length sortlst <> 1
+        then raise (C.CoAlgException "=-formula is used in wrong sort.")
+        else ();
+    | C.HCCONSTN _ ->
+      if func <> Constant || List.length sortlst <> 1
+        then raise (C.CoAlgException "=-formula is used in wrong sort.")
+        else ();
+      (* NB: =-formulae have no subformlae hence no closure *)
     | C.HCCHC (f1, f2)
     | C.HCCHCN (f1, f2) ->
         if func <> Choice || List.length sortlst <> 2 then
@@ -797,6 +811,32 @@ let initTables nomTbl hcF htF htR s f n =
       !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
       !arrayDestNum.(s).(n) <- p.C.nominator;
       !arrayDestNum2.(s).(n) <- p.C.denominator
+  | C.HCCONST str ->
+      !arrayType.(s).(n) <- ConstF; (* type of modality *)
+      (* Dest1 and Dest2 are the arguments, here: none *)
+      (* DestNum and DestNum2 are the numerators and denonimators of
+      fractions, here: none *)
+      !arrayDest3.(s).(n) <-
+        if Hashtbl.mem htR str then Hashtbl.find htR str
+        else
+          let size = Hashtbl.length htR in
+          Hashtbl.add htR str size;
+          size
+      (* Dest3 are the role names / identifiers for constant values *)
+      (* idea: hash identifier names *)
+  | C.HCCONSTN str ->
+      !arrayType.(s).(n) <- ConstnF; (* type of modality *)
+      (* Dest1 and Dest2 are the arguments, here: none *)
+      (* DestNum and DestNum2 are the numerators and denonimators of
+      fractions, here: none *)
+      !arrayDest3.(s).(n) <-
+        if Hashtbl.mem htR str then Hashtbl.find htR str
+        else
+          let size = Hashtbl.length htR in
+          Hashtbl.add htR str size;
+          size
+      (* Dest3 are the role names / identifiers for constant values *)
+      (* idea: hash identifier names *)
   | C.HCCHC (f1, f2)
   | C.HCCHCN (f1, f2) ->
       !arrayType.(s).(n) <- ChcF;
diff --git a/src/lib/CoAlgMisc.mli b/src/lib/CoAlgMisc.mli
index 58821f43f189063563f87d8127f7902321dee266..9eab31cf0c2855ebc12decd55e0d1ea55741c0e1 100644
--- a/src/lib/CoAlgMisc.mli
+++ b/src/lib/CoAlgMisc.mli
@@ -15,6 +15,7 @@ type functors =
   | CoalitionLogic
   | GML
   | PML
+  | Constant
   | Choice
   | Fusion
 
@@ -38,6 +39,8 @@ type formulaType =
   | MaxExceptF
   | AtLeastProbF (* diamond for PML *)
   | LessProbFailF (* box for PML *)
+  | ConstF (* constant functor *)
+  | ConstnF (* constant functor *)
   | ChcF
   | FusF