From c5c25acf29323ee25e7ab9b685c912dc100db7e4 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Mon, 7 Dec 2015 16:53:11 +0100
Subject: [PATCH] Whitespace cleanup
No tabs any more
---
src/lib/CoAlgFormula.ml | 404 ++++++++++++++++++++--------------------
1 file changed, 202 insertions(+), 202 deletions(-)
diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index 41ce1ce..bb942a6 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -12,7 +12,7 @@ module Str = String
(** A general exception for all kinds of errors
that can happen in the tableau procedure.
- More specific information is given in the argument.
+ More specific information is given in the argument.
*)
exception CoAlgException of string
@@ -48,7 +48,7 @@ type formula =
| MORETHAN of int * string * formula (* diamond of GML *)
| MAXEXCEPT of int * string * formula (* box of GML *)
| ATLEASTPROB of rational * formula (* = {>= 0.5} C ---> C occurs with *)
- (* probability of at least 50% *)
+ (* 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 *)
@@ -89,14 +89,14 @@ let isNominal s = String.contains s '\''
*)
let rec sizeFormula f =
match f with
- | TRUE
- | FALSE
+ | TRUE
+ | FALSE
| AP _ -> 1
| NOT f1
| AT (_, f1) -> succ (sizeFormula f1)
- | OR (f1, f2)
+ | OR (f1, f2)
| AND (f1, f2)
- | EQU (f1, f2)
+ | EQU (f1, f2)
| IMP (f1, f2) -> succ (sizeFormula f1 + sizeFormula f2)
| EX (_, f1)
| AX (_, f1)
@@ -121,7 +121,7 @@ let rec sizeFormula f =
| AF _ | EF _
| AG _ | EG _
| AU _ | EU _ ->
- raise (CoAlgException ("sizeFormula: CTL should have been removed at this point"))
+ raise (CoAlgException ("sizeFormula: CTL should have been removed at this point"))
(** Determines the size of a sorted formula.
@param f A sorted formula.
@@ -229,21 +229,21 @@ let gensym = Stream.from (fun i -> Some (Printf.sprintf "#gensym%x#" i))
let convertToMu formula =
let helper formula =
- let symbol = Stream.next gensym in
- match formula with
- | AF f1 ->
- MU (symbol, (OR (f1, (AX ("", (VAR symbol))))))
- | EF f1 ->
- MU (symbol, (OR (f1, (EX ("", (VAR symbol))))))
- | AG f1 ->
- NU (symbol, (AND (f1, (AX ("", (VAR symbol))))))
- | EG f1 ->
- NU (symbol, (AND (f1, (EX ("", (VAR symbol))))))
- | AU (f1, f2) ->
- MU (symbol, (OR (f2, (AND (f1, (AX ("", (VAR symbol))))))))
- | EU (f1, f2) ->
- MU (symbol, (OR (f2, (AND (f1, (EX ("", (VAR symbol))))))))
- | _ -> formula
+ let symbol = Stream.next gensym in
+ match formula with
+ | AF f1 ->
+ MU (symbol, (OR (f1, (AX ("", (VAR symbol))))))
+ | EF f1 ->
+ MU (symbol, (OR (f1, (EX ("", (VAR symbol))))))
+ | AG f1 ->
+ NU (symbol, (AND (f1, (AX ("", (VAR symbol))))))
+ | EG f1 ->
+ NU (symbol, (AND (f1, (EX ("", (VAR symbol))))))
+ | AU (f1, f2) ->
+ MU (symbol, (OR (f2, (AND (f1, (AX ("", (VAR symbol))))))))
+ | EU (f1, f2) ->
+ MU (symbol, (OR (f2, (AND (f1, (EX ("", (VAR symbol))))))))
+ | _ -> formula
in
convert_post helper formula
@@ -261,7 +261,7 @@ let rec exportFormula_buffer sb f =
let prio n lf =
let prionr = function
| EQU _ -> 0
- | IMP _ -> 1
+ | IMP _ -> 1
| OR _ -> 2
| AND _ -> 3
| _ -> 4
@@ -402,35 +402,35 @@ let rec exportFormula_buffer sb f =
prio 4 f1
| NU (s, f1) ->
Buffer.add_string sb "ν";
- Buffer.add_string sb s;
+ Buffer.add_string sb s;
Buffer.add_string sb ".";
prio 4 f1
| VAR s ->
Buffer.add_string sb s
| AF f1 ->
- Buffer.add_string sb "AF ";
- prio 4 f1
+ Buffer.add_string sb "AF ";
+ prio 4 f1
| EF f1 ->
- Buffer.add_string sb "EF ";
- prio 4 f1
+ Buffer.add_string sb "EF ";
+ prio 4 f1
| AG f1 ->
- Buffer.add_string sb "AG ";
- prio 4 f1
+ Buffer.add_string sb "AG ";
+ prio 4 f1
| EG f1 ->
- Buffer.add_string sb "EG ";
- prio 4 f1
+ Buffer.add_string sb "EG ";
+ prio 4 f1
| AU (f1, f2) ->
- Buffer.add_string sb "A (";
- prio 4 f1;
- Buffer.add_string sb " U ";
- prio 4 f2;
- Buffer.add_string sb ")"
+ Buffer.add_string sb "A (";
+ prio 4 f1;
+ Buffer.add_string sb " U ";
+ prio 4 f2;
+ Buffer.add_string sb ")"
| EU (f1, f2) ->
- Buffer.add_string sb "E (";
- prio 4 f1;
- Buffer.add_string sb " U ";
- prio 4 f2;
- Buffer.add_string sb ")"
+ Buffer.add_string sb "E (";
+ prio 4 f1;
+ Buffer.add_string sb " U ";
+ prio 4 f2;
+ Buffer.add_string sb ")"
(** Converts a formula into a string representation.
Parentheses are ommited where possible
@@ -450,7 +450,7 @@ let rec exportTatlFormula_buffer sb f =
let prio n lf =
let prionr = function
| EQU _ -> 0
- | IMP _ -> 1
+ | IMP _ -> 1
| OR _ -> 2
| AND _ -> 3
| _ -> 4
@@ -597,12 +597,12 @@ let exportQueryParsable tbox (_,f) =
(* NB: True and False are the propositional constants. Lower case
true/false are regardes as atomic propositions and we emit a warning
*)
-let lexer = A.make_lexer
+let lexer = A.make_lexer
[":";";";"|-";"(";")";"=>";"<=>";"|";"&";"~";"@";"True";"False";"true";"false";"<";">";"[";"]";"{<=";"{>=";"}";"+";"[pi1]";"[pi2]"
;"[{";"}]";"<{";"}>";",";"/";"{<";"=";"=o";"O"
;"μ";"ν";"."
- ;"AX";"EX";"AF";"EF";"AG";"EG";"A";"E";"U"
- ]
+ ;"AX";"EX";"AF";"EF";"AG";"EG";"A";"E";"U"
+ ]
let mk_exn s = CoAlgException s
@@ -620,15 +620,15 @@ let rec verifyMuAltFree formula =
| EX (_,a) | AX (_,a) -> proc a
| OR (a,b) | AND (a,b)
| EQU (a,b) | IMP (a,b) ->
- let (atype, afree) = proc a
- and (btype, bfree) = proc b in
- if (compare atype "μ" == 0 && compare btype "ν" == 0) ||
- (compare atype "ν" == 0 && compare btype "μ" == 0) then
- raise (CoAlgException ("formula not alternation-free"));
- if compare atype "none" == 0 then
- (btype, List.flatten [afree; bfree])
- else
- (atype, List.flatten [afree; bfree])
+ let (atype, afree) = proc a
+ and (btype, bfree) = proc b in
+ if (compare atype "μ" == 0 && compare btype "ν" == 0) ||
+ (compare atype "ν" == 0 && compare btype "μ" == 0) then
+ raise (CoAlgException ("formula not alternation-free"));
+ if compare atype "none" == 0 then
+ (btype, List.flatten [afree; bfree])
+ else
+ (atype, List.flatten [afree; bfree])
| ENFORCES (_,a) | ALLOWS (_,a)
| MIN (_,_,a) | MAX (_,_,a)
| ATLEASTPROB (_, a) | LESSPROBFAIL (_, a)
@@ -636,39 +636,39 @@ let rec verifyMuAltFree formula =
| ID(a) -> proc a
| NORM(a, b) | NORMN(a, b)
| CHC (a,b) ->
- let (atype, afree) = proc a
- and (btype, bfree) = proc b in
- if (compare atype "μ" == 0 && compare btype "ν" == 0) ||
- (compare atype "ν" == 0 && compare btype "μ" == 0) then
- raise (CoAlgException ("formula not alternation-free"));
- if compare atype "none" == 0 then
- (btype, List.flatten [afree; bfree])
- else
- (atype, List.flatten [afree; bfree])
+ let (atype, afree) = proc a
+ and (btype, bfree) = proc b in
+ if (compare atype "μ" == 0 && compare btype "ν" == 0) ||
+ (compare atype "ν" == 0 && compare btype "μ" == 0) then
+ raise (CoAlgException ("formula not alternation-free"));
+ if compare atype "none" == 0 then
+ (btype, List.flatten [afree; bfree])
+ else
+ (atype, List.flatten [afree; bfree])
| FUS (_,a) -> proc a
| MU (s, f) ->
- let (fptype, free) = proc f in
- (if (compare fptype "ν" == 0) then
- raise (CoAlgException ("formula not alternation-free")));
- let predicate x = compare x s != 0 in
+ let (fptype, free) = proc f in
+ (if (compare fptype "ν" == 0) then
+ raise (CoAlgException ("formula not alternation-free")));
+ let predicate x = compare x s != 0 in
let newfree = List.filter predicate free in
- if newfree = [] then
- ("none", [])
- else
- ("μ", newfree)
+ if newfree = [] then
+ ("none", [])
+ else
+ ("μ", newfree)
| NU (s, f) ->
- let (fptype, free) = proc f in
- (if (compare fptype "μ" == 0) then
- raise (CoAlgException ("formula not alternation-free")));
- let predicate x = compare x s != 0 in
+ let (fptype, free) = proc f in
+ (if (compare fptype "μ" == 0) then
+ raise (CoAlgException ("formula not alternation-free")));
+ let predicate x = compare x s != 0 in
let newfree = List.filter predicate free in
- if newfree = [] then
- ("none", [])
- else
- ("ν", newfree)
+ if newfree = [] then
+ ("none", [])
+ else
+ ("ν", newfree)
| VAR s -> ("none", [s])
| AF _ | EF _ | AG _ | EG _ | AU _ | EU _ ->
- raise (CoAlgException ("verifyMuAltFree: CTL should have been removed at this point"))
+ raise (CoAlgException ("verifyMuAltFree: CTL should have been removed at this point"))
(** Process from outside in. For every variable bound keep the tuple
@@ -696,18 +696,18 @@ let rec verifyMuMonotone negations formula =
| FUS (_,a) -> proc a
| MU (s, f)
| NU (s, f) ->
- let newNeg = (s, 0) :: negations in
- verifyMuMonotone newNeg f
+ let newNeg = (s, 0) :: negations in
+ verifyMuMonotone newNeg f
| VAR s ->
- let finder (x, _) = compare x s == 0 in
- let (_, neg) = List.find finder negations in
- if ((neg land 1) != 0) then raise (CoAlgException ("formula not monotone"))
+ let finder (x, _) = compare x s == 0 in
+ let (_, neg) = List.find finder negations in
+ if ((neg land 1) != 0) then raise (CoAlgException ("formula not monotone"))
| NOT a ->
- let increment (s, n) = (s, n+1) in
- let newNeg = List.map increment negations in
- verifyMuMonotone newNeg a
+ let increment (s, n) = (s, n+1) in
+ let newNeg = List.map increment negations in
+ verifyMuMonotone newNeg a
| AF _ | EF _ | AG _ | EG _ | AU _ | EU _ ->
- raise (CoAlgException ("verifyMuMonotone: CTL should have been removed at this point"))
+ raise (CoAlgException ("verifyMuMonotone: CTL should have been removed at this point"))
let rec verifyMuGuarded unguarded formula =
let proc = verifyMuGuarded unguarded in
@@ -729,14 +729,14 @@ let rec verifyMuGuarded unguarded formula =
| FUS (_,a) -> proc a
| MU (s, f)
| NU (s, f) ->
- let newUnguard = s :: unguarded in
- verifyMuGuarded newUnguard f
+ let newUnguard = s :: unguarded in
+ verifyMuGuarded newUnguard f
| VAR s ->
- let finder x = compare x s == 0 in
- if List.exists finder unguarded then
- raise (CoAlgException ("formula not guarded"))
+ let finder x = compare x s == 0 in
+ if List.exists finder unguarded then
+ raise (CoAlgException ("formula not guarded"))
| AF _ | EF _ | AG _ | EG _ | AU _ | EU _ ->
- raise (CoAlgException ("verifyMuGuarded: CTL should have been removed at this point"))
+ raise (CoAlgException ("verifyMuGuarded: CTL should have been removed at this point"))
let verifyFormula formula =
verifyMuAltFree formula;
@@ -885,11 +885,11 @@ and parse_rest symtab ts =
| A.Kwd "True" -> TRUE
| A.Kwd "False" -> FALSE
| A.Ident s ->
- (try
- let finder (x, _) = compare x s == 0 in
- let (_, symbol) = List.find finder symtab in
- VAR symbol
- with Not_found -> AP s)
+ (try
+ let finder (x, _) = compare x s == 0 in
+ let (_, symbol) = List.find finder symtab in
+ VAR symbol
+ with Not_found -> AP s)
| A.Kwd "~" ->
let f = parse_rest symtab ts in
NOT f
@@ -901,35 +901,35 @@ and parse_rest symtab ts =
in
let f = parse_rest symtab ts in
AT (s, f)
- | A.Kwd "<" ->
+ | A.Kwd "<" ->
let (_, _, s) = boxinternals true ">" in
let f1 = parse_rest symtab ts in
- EX (s, f1)
- | A.Kwd "[" ->
+ EX (s, f1)
+ | A.Kwd "[" ->
let (_, _, s) = boxinternals true "]" in
let f1 = parse_rest symtab ts in
AX (s, f1)
- | A.Kwd "[{" ->
+ | A.Kwd "[{" ->
let ls = agentlist "}]" in
let f1 = parse_rest symtab ts in
ENFORCES (ls, f1)
- | A.Kwd "<{" ->
+ | A.Kwd "<{" ->
let ls = agentlist "}>" in
let f1 = parse_rest symtab ts in
ALLOWS (ls, f1)
- | A.Kwd "{>=" ->
+ | A.Kwd "{>=" ->
let (n, denom, s) = boxinternals false "}" in
let f1 = parse_rest symtab ts in
if (denom <> 0)
then ATLEASTPROB (rational_of_int n denom, f1)
else MIN (n, s, f1)
- | A.Kwd "{<=" ->
+ | A.Kwd "{<=" ->
let (n, denom, s) = boxinternals false "}" in
let f1 = parse_rest symtab ts in
if (denom <> 0)
then A.printError mk_exn ~ts "Can not express {<= probability}"
else MAX (n, s, f1)
- | A.Kwd "{<" ->
+ | A.Kwd "{<" ->
let (n, denom, s) = boxinternals false "}" in
let f1 = parse_rest symtab ts in
if (denom <> 0)
@@ -965,49 +965,49 @@ and parse_rest symtab ts =
FUS (false, f)
| A.Kwd "μ" ->
let (_, _, s) = boxinternals true "." in
- let symbol = Stream.next gensym in
- let newtab = (s, symbol) :: symtab in
+ let symbol = Stream.next gensym in
+ let newtab = (s, symbol) :: symtab in
let f1 = parse_rest newtab ts in
MU (symbol, f1)
| A.Kwd "ν" ->
let (_, _, s) = boxinternals true "." in
- let symbol = Stream.next gensym in
- let newtab = (s, symbol) :: symtab in
+ let symbol = Stream.next gensym in
+ let newtab = (s, symbol) :: symtab in
let f1 = parse_rest newtab ts in
NU (symbol, f1)
| A.Kwd "AF" ->
- let f = parse_rest symtab ts in
- AF f
+ let f = parse_rest symtab ts in
+ AF f
| A.Kwd "EF" ->
- let f = parse_rest symtab ts in
- EF f
+ let f = parse_rest symtab ts in
+ EF f
| A.Kwd "AG" ->
- let f = parse_rest symtab ts in
- AG f
+ let f = parse_rest symtab ts in
+ AG f
| A.Kwd "EG" ->
- let f = parse_rest symtab ts in
- EG f
+ let f = parse_rest symtab ts in
+ EG f
| A.Kwd "A" ->
- assert (Stream.next ts = A.Kwd "(");
- let f1 = parse_formula symtab ts in
- assert (Stream.next ts = A.Kwd "U");
- let f2 = parse_formula symtab ts in
- assert (Stream.next ts = A.Kwd ")");
- AU (f1, f2)
+ assert (Stream.next ts = A.Kwd "(");
+ let f1 = parse_formula symtab ts in
+ assert (Stream.next ts = A.Kwd "U");
+ let f2 = parse_formula symtab ts in
+ assert (Stream.next ts = A.Kwd ")");
+ AU (f1, f2)
| A.Kwd "E" ->
- assert (Stream.next ts = A.Kwd "(");
- let f1 = parse_formula symtab ts in
- assert (Stream.next ts = A.Kwd "U");
- let f2 = parse_formula symtab ts in
- assert (Stream.next ts = A.Kwd ")");
- EU (f1, f2)
+ assert (Stream.next ts = A.Kwd "(");
+ let f1 = parse_formula symtab ts in
+ assert (Stream.next ts = A.Kwd "U");
+ let f2 = parse_formula symtab ts in
+ assert (Stream.next ts = A.Kwd ")");
+ EU (f1, f2)
| A.Kwd "AX" ->
- let f1 = parse_rest symtab ts in
- AX ("", f1)
+ let f1 = parse_rest symtab ts in
+ AX ("", f1)
| A.Kwd "EX" ->
- let f1 = parse_rest symtab ts in
- EX ("", f1)
- | t -> A.printError mk_exn ~t ~ts
+ let f1 = parse_rest symtab ts in
+ EX ("", f1)
+ | t -> A.printError mk_exn ~t ~ts
"\"<\", \"[\", \"{>=\", \"{<=\", \"@\", \"~\", \"(\",
\"True\", \"False\", \"=\", \"=o\", \"O\" or <ident> expected: "
@@ -1017,7 +1017,7 @@ and parse_rest symtab ts =
@raise CoAlgException If ts does not represent a sorted formula.
*)
let parse_sortedFormula ts =
- let nr =
+ let nr =
match Stream.peek ts with
| Some (A.Int n) ->
if n >= 0 then begin
@@ -1030,7 +1030,7 @@ let parse_sortedFormula ts =
n
end else
A.printError mk_exn ~ts ("<non-negative number> expected: ")
- | _ -> 0
+ | _ -> 0
in
let f = parse_formula [] ts in
(nr, f)
@@ -1102,7 +1102,7 @@ let importQuery s =
Stream.junk ts;
let f = parse_sortedFormula ts in
(fl, f)
- | _ ->
+ | _ ->
if List.length fl = 1 then ([], List.hd fl)
else A.printError mk_exn ~ts "\"|-\" expected: "
in
@@ -1143,7 +1143,7 @@ let rec nnfNeg f =
| ID (f1) -> ID (nnfNeg f1)
| NORM(f1, f2) -> NORMN(nnfNeg f1, nnfNeg f2)
| NORMN(f1, f2) -> NORM (nnfNeg f1, nnfNeg f2)
- | CHC (f1, f2) -> CHC (nnfNeg f1, nnfNeg f2)
+ | CHC (f1, f2) -> CHC (nnfNeg f1, nnfNeg f2)
| FUS (first, f1) -> FUS (first, nnfNeg f1)
| MU (s, f1) -> NU(s, nnfNeg f1)
| NU (s, f1) -> MU(s, nnfNeg f1)
@@ -1153,7 +1153,7 @@ let rec nnfNeg f =
| EG _
| AU _
| EU _ -> raise (CoAlgException ("nnfNeg: CTL should have been removed at this point"))
-
+
(** Converts a formula to negation normal form
by "pushing in" the negations "~".
The symbols "<=>" and "=>" are substituted by their usual definitions.
@@ -1184,13 +1184,13 @@ and nnf f =
if ft1 == f1 && ft2 == f2 then f else AND (ft1, ft2)
| EQU (f1, f2) -> AND (OR (nnfNeg f1, nnf f2), OR (nnfNeg f2, nnf f1))
| IMP (f1, f2) -> OR (nnfNeg f1, nnf f2)
- | EX (s, f1) ->
+ | EX (s, f1) ->
let ft = nnf f1 in
if ft == f1 then f else EX (s, ft)
| AX (s, f1) ->
let ft = nnf f1 in
if ft == f1 then f else AX (s, ft)
- | ENFORCES (s, f1) ->
+ | ENFORCES (s, f1) ->
let ft = nnf f1 in
if ft == f1 then f else ENFORCES (s, ft)
| ALLOWS (s, f1) ->
@@ -1279,7 +1279,7 @@ let rec simplify f =
| _, TRUE -> TRUE
| _, FALSE -> ft1
| _, _ ->
- if (f1 == ft1) && (f2 == ft2) then f
+ if (f1 == ft1) && (f2 == ft2) then f
else OR (ft1, ft2)
end
| AND (f1, f2) ->
@@ -1292,7 +1292,7 @@ let rec simplify f =
| _, TRUE -> ft1
| _, FALSE -> FALSE
| _, _ ->
- if (f1 == ft1) && (f2 == ft2) then f
+ if (f1 == ft1) && (f2 == ft2) then f
else AND (ft1, ft2)
end
| NOT _
@@ -1384,7 +1384,7 @@ let rec simplify f =
match ft2 with
| TRUE -> TRUE
| _ ->
- if (f1 == ft1) && (f2 == ft2) then f
+ if (f1 == ft1) && (f2 == ft2) then f
else NORM (ft1, ft2)
end
| NORMN (f1, f2) ->
@@ -1394,7 +1394,7 @@ let rec simplify f =
match ft2 with
| FALSE -> FALSE
| _ ->
- if (f1 == ft1) && (f2 == ft2) then f
+ if (f1 == ft1) && (f2 == ft2) then f
else NORMN (ft1, ft2)
end
| CHC (f1, f2) ->
@@ -1405,7 +1405,7 @@ let rec simplify f =
| TRUE, TRUE -> TRUE
| FALSE, FALSE -> FALSE
| _, _ ->
- if (f1 == ft1) && (f2 == ft2) then f
+ if (f1 == ft1) && (f2 == ft2) then f
else CHC (ft1, ft2)
end
| FUS (first, f1) ->
@@ -1423,7 +1423,7 @@ let rec simplify f =
| EG _
| AU _
| EU _ ->
- raise (CoAlgException ("nnf: CTL should have been removed at this point"))
+ raise (CoAlgException ("nnf: CTL should have been removed at this point"))
(** Destructs an atomic proposition.
@param f An atomic proposition.
@@ -1714,7 +1714,7 @@ let is_fusion f =
| FUS _ -> true
| _ -> false
-
+
(** The constant True.
*)
let const_true = TRUE
@@ -1722,7 +1722,7 @@ let const_true = TRUE
(** The constant False.
*)
let const_false = FALSE
-
+
(** Constructs an atomic proposition.
@param s The name of the atomic proposition.
@return The atomic proposition with name s.
@@ -1746,7 +1746,7 @@ let const_nom s =
@return The negation of f.
*)
let const_not f = NOT f
-
+
(** Constructs an @-formula from a name and a formula.
@param s A nominal name.
@param f A formula.
@@ -1765,7 +1765,7 @@ let const_or f1 f2 = OR (f1, f2)
@param f1 The first formula (LHS).
@param f2 The second formula (LHS).
@return The formula f1 & f2.
- *)
+ *)
let const_and f1 f2 = AND (f1, f2)
(** Constructs an equivalence from two formulae.
@@ -1895,7 +1895,7 @@ let equal_hcFormula_node f1 f2 =
| HCALLOWS (s1, f1), HCALLOWS (s2, f2) -> compare s1 s2 = 0 && f1 == f2
| HCMORETHAN (n1, s1, f1), HCMORETHAN (n2, s2, f2)
| HCMAXEXCEPT (n1, s1, f1), HCMAXEXCEPT (n2, s2, f2) ->
- n1 = n2 && compare s1 s2 = 0 && f1 == f2
+ n1 = n2 && compare s1 s2 = 0 && f1 == f2
| HCATLEASTPROB (p1, f1), HCATLEASTPROB (p2,f2) ->
p1 = p2 && f1 == f2
| HCLESSPROBFAIL (p1, f1), HCLESSPROBFAIL (p2,f2) ->
@@ -2120,18 +2120,18 @@ let rec hc_formula hcF f =
let tf1 = hc_formula hcF f1 in
HcFormula.hashcons hcF (HCFUS (first, tf1))
| MU (var, f1) ->
- let tf1 = hc_formula hcF f1 in
- HcFormula.hashcons hcF (HCMU (var, tf1))
+ let tf1 = hc_formula hcF f1 in
+ HcFormula.hashcons hcF (HCMU (var, tf1))
| NU (var, f1) ->
- let tf1 = hc_formula hcF f1 in
- HcFormula.hashcons hcF (HCNU (var, tf1))
+ let tf1 = hc_formula hcF f1 in
+ HcFormula.hashcons hcF (HCNU (var, tf1))
| AF _
| EF _
| AG _
| EG _
| AU _
| EU _ ->
- raise (CoAlgException ("nnf: CTL should have been removed at this point"))
+ raise (CoAlgException ("nnf: CTL should have been removed at this point"))
(* Replace the Variable name in f with formula formula
hc_replace foo φ ψ => ψ[foo |-> φ]
@@ -2147,74 +2147,74 @@ let rec hc_replace hcF name (formula: hcFormula) (f: hcFormula) =
| HCCONST _
| HCCONSTN _ -> f
| HCVAR s ->
- if compare s name == 0
- then formula
- else f
+ if compare s name == 0
+ then formula
+ else f
| HCAT (s, f1) ->
- let nf1 = func f1 in
- if nf1 == f1 then f else gennew (HCAT(s, nf1))
+ let nf1 = func f1 in
+ if nf1 == f1 then f else gennew (HCAT(s, nf1))
| HCOR (f1, f2) ->
- let nf1 = func f1 in
- let nf2 = func f2 in
- if nf1 == f1 && nf2 == f2 then f else gennew (HCOR(nf1, nf2))
+ let nf1 = func f1 in
+ let nf2 = func f2 in
+ if nf1 == f1 && nf2 == f2 then f else gennew (HCOR(nf1, nf2))
| HCAND (f1, f2) ->
- let nf1 = func f1 in
- let nf2 = func f2 in
- if nf1 == f1 && nf2 == f2 then f else gennew (HCAND(nf1, nf2))
+ let nf1 = func f1 in
+ let nf2 = func f2 in
+ if nf1 == f1 && nf2 == f2 then f else gennew (HCAND(nf1, nf2))
| HCEX (s, f1) ->
- let nf1 = func f1 in
- if nf1 == f1 then f else gennew (HCEX(s, nf1))
+ let nf1 = func f1 in
+ if nf1 == f1 then f else gennew (HCEX(s, nf1))
| HCAX (s, f1) ->
let nf1 = func f1 in
- if nf1 == f1 then f else gennew (HCAX(s, nf1))
+ if nf1 == f1 then f else gennew (HCAX(s, nf1))
| HCENFORCES (s, f1) ->
- let nf1 = func f1 in
- if nf1 == f1 then f else gennew (HCENFORCES(s, nf1))
+ let nf1 = func f1 in
+ if nf1 == f1 then f else gennew (HCENFORCES(s, nf1))
| HCALLOWS (s, f1) ->
let nf1 = func f1 in
- if nf1 == f1 then f else gennew (HCALLOWS(s, nf1))
+ if nf1 == f1 then f else gennew (HCALLOWS(s, nf1))
| HCMORETHAN (n, s, f1) ->
let nf1 = func f1 in
- if nf1 == f1 then f else gennew (HCMORETHAN(n, s, nf1))
+ if nf1 == f1 then f else gennew (HCMORETHAN(n, s, nf1))
| HCMAXEXCEPT (n, s, f1) ->
- let nf1 = func f1 in
- if nf1 == f1 then f else gennew (HCMAXEXCEPT(n, s, nf1))
+ let nf1 = func f1 in
+ if nf1 == f1 then f else gennew (HCMAXEXCEPT(n, s, nf1))
| HCATLEASTPROB (p, f1) ->
let nf1 = func f1 in
- if nf1 == f1 then f else gennew (HCATLEASTPROB(p, nf1))
+ if nf1 == f1 then f else gennew (HCATLEASTPROB(p, nf1))
| HCLESSPROBFAIL (p, f1) ->
let nf1 = func f1 in
- if nf1 == f1 then f else gennew (HCLESSPROBFAIL(p, nf1))
+ if nf1 == f1 then f else gennew (HCLESSPROBFAIL(p, nf1))
| HCID f1 ->
let nf1 = func f1 in
- if nf1 == f1 then f else gennew (HCID(nf1))
+ if nf1 == f1 then f else gennew (HCID(nf1))
| HCNORM (f1, f2) ->
- let nf1 = func f1 in
- let nf2 = func f2 in
- if nf1 == f1 && nf2 == f2 then f else gennew (HCNORM(nf1, nf2))
+ let nf1 = func f1 in
+ let nf2 = func f2 in
+ if nf1 == f1 && nf2 == f2 then f else gennew (HCNORM(nf1, nf2))
| HCNORMN (f1, f2) ->
- let nf1 = func f1 in
- let nf2 = func f2 in
- if nf1 == f1 && nf2 == f2 then f else gennew (HCNORMN(nf1, nf2))
+ let nf1 = func f1 in
+ let nf2 = func f2 in
+ if nf1 == f1 && nf2 == f2 then f else gennew (HCNORMN(nf1, nf2))
| HCCHC (f1, f2) ->
- let nf1 = func f1 in
- let nf2 = func f2 in
- if nf1 == f1 && nf2 == f2 then f else gennew (HCCHC(nf1, nf2))
+ let nf1 = func f1 in
+ let nf2 = func f2 in
+ if nf1 == f1 && nf2 == f2 then f else gennew (HCCHC(nf1, nf2))
| HCFUS (first, f1) ->
let nf1 = func f1 in
- if nf1 == f1 then f else gennew (HCFUS(first, nf1))
+ if nf1 == f1 then f else gennew (HCFUS(first, nf1))
| HCMU (var, f1) ->
- if compare var name != 0 then
+ if compare var name != 0 then
let nf1 = func f1 in
- if nf1 == f1 then f else gennew (HCMU(var, nf1))
- else
- f
+ if nf1 == f1 then f else gennew (HCMU(var, nf1))
+ else
+ f
| HCNU (var, f1) ->
- if compare var name != 0 then
+ if compare var name != 0 then
let nf1 = func f1 in
- if nf1 == f1 then f else gennew (HCNU(var, nf1))
- else
- f
+ if nf1 == f1 then f else gennew (HCNU(var, nf1))
+ else
+ f
(** An instantiation of a hash table (of the standard library)
--
GitLab