[bpt/coccinelle.git] / ctl / test_ctl.ml

(*
 * Copyright 2010, INRIA, University of Copenhagen
 * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix
 * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
 * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
 * This file is part of Coccinelle.
 *
 * Coccinelle is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, according to version 2 of the License.
 *
 * Coccinelle is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Coccinelle.  If not, see <http://www.gnu.org/licenses/>.
 *
 * The authors reserve the right to distribute this or future versions of
 * Coccinelle under other licenses.
 *)


(*
 * Copyright 2010, INRIA, University of Copenhagen
 * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix
 * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
 * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
 * This file is part of Coccinelle.
 *
 * Coccinelle is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, according to version 2 of the License.
 *
 * Coccinelle is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Coccinelle.  If not, see <http://www.gnu.org/licenses/>.
 *
 * The authors reserve the right to distribute this or future versions of
 * Coccinelle under other licenses.
 *)


(* ********************************************************************** *)
(* Module: EXAMPLE_ENGINE (instance of CTL_ENGINE)                        *)
(* ********************************************************************** *)

(* Simple env.: meta.vars and values are strings *)
module SIMPLE_ENV =
  struct
    type value = string;;
    type mvar = string;;
    let eq_mvar x x' = x = x';;
    let eq_val v v' = v = v';;
    let merge_val v v' = v;;
  end
;;

(* Simple predicates *)
module WRAPPER_PRED =
  struct
    type predicate = string
  end

module EXAMPLE_ENGINE =
  Wrapper_ctl.CTL_ENGINE_BIS (SIMPLE_ENV) (Ctl_engine.OGRAPHEXT_GRAPH) (WRAPPER_PRED)

let top_wit = []

(* ******************************************************************** *)
(*                                                                      *)
(* EXAMPLES                                                             *)
(*                                                                      *)
(* ******************************************************************** *)

(* For convenience in the examples *)
(* FIX ME: remove *)
open Ctl_engine.OGRAPHEXT_GRAPH;;
open EXAMPLE_ENGINE;;
open Ast_ctl;;

(* ---------------------------------------------------------------------- *)
(* Helpers                                                                *)
(* ---------------------------------------------------------------------- *)

(* FIX ME: move to ENGINE module *)
let (-->) x v = Subst (x,v);;

(* FIX ME: move to ENGINE module *)
let (-/->) x v = NegSubst(x,v);;

let mkgraph nodes edges =
  let g = ref (new Ograph_extended.ograph_extended) in
  let addn (n,x) =
    (* let (g',i) = (!g)#add_node x in *)
    (* now I need to force the nodei of a node, because of the state(vx) predicates
       hence add_node -> add_nodei
     *)
    let (g', i) = !g#add_nodei n x in
    assert (i = n);
    g := g'; (n,i) in
  let adde anodes (n1,n2,x) =
    let g' = (!g)#add_arc ((List.assoc n1 anodes,List.assoc n2 anodes),x) in
    g := g'; () in
  let add_nodes = List.map addn nodes in
  let _add_edges = List.map (adde add_nodes) edges in
  !g
;;


(* CTL parameterised on basic predicates and metavar's*)
type ('pred,'mvar) old_gen_ctl =
  | False_
  | True_
  | Pred_ of 'pred
  | Not_ of ('pred,'mvar) old_gen_ctl
  | Exists_ of 'mvar * ('pred,'mvar) old_gen_ctl		(* !!! *)
  | And_ of ('pred,'mvar) old_gen_ctl * ('pred,'mvar) old_gen_ctl
  | Or_  of ('pred,'mvar) old_gen_ctl * ('pred,'mvar) old_gen_ctl
  | Implies_ of ('pred,'mvar) old_gen_ctl * ('pred,'mvar) old_gen_ctl
  | AF_ of ('pred,'mvar) old_gen_ctl
  | AX_ of ('pred,'mvar) old_gen_ctl
  | AG_ of ('pred,'mvar) old_gen_ctl
  | AU_ of ('pred,'mvar) old_gen_ctl * ('pred,'mvar) old_gen_ctl
  | EF_ of ('pred,'mvar) old_gen_ctl
  | EX_ of ('pred,'mvar) old_gen_ctl
  | EG_ of ('pred,'mvar) old_gen_ctl
  | EU_ of ('pred,'mvar) old_gen_ctl * ('pred,'mvar) old_gen_ctl
  | Let_ of string * ('pred,'mvar) old_gen_ctl * ('pred,'mvar) old_gen_ctl
  | Ref_ of string

let rec mkanno phi0 =
  let anno phi = (phi,None) in
  match phi0 with
    | False_              -> anno False
    | True_               -> anno True
    | Pred_(p)            -> anno (Pred(p))
    | Not_(phi)           -> anno (Not(mkanno phi))
    | Exists_(v,phi)      -> anno (Exists(v,mkanno phi))
    | And_(phi1,phi2)     -> anno (And(mkanno phi1,mkanno phi2))
    | Or_(phi1,phi2)      -> anno (Or(mkanno phi1,mkanno phi2))
    | Implies_(phi1,phi2) -> anno (Implies(mkanno phi1,mkanno phi2))
    | AF_(phi1)           -> anno (AF(mkanno phi1))
    | AX_(phi1)           -> anno (AX(mkanno phi1))
    | AG_(phi1)           -> anno (AG(mkanno phi1))
    | AU_(phi1,phi2)      -> anno (AU(mkanno phi1,mkanno phi2))
    | EF_(phi1)           -> anno (EF(mkanno phi1))
    | EX_(phi1)		  -> anno (EX(mkanno phi1))
    | EG_(phi1)		  -> anno (EG(mkanno phi1))
    | EU_(phi1,phi2)	  -> anno (EU(mkanno phi1,mkanno phi2))
    | Let_ (x,phi1,phi2)  -> anno (Let(x,mkanno phi1,mkanno phi2))
    | Ref_(s)             -> anno (Ref(s))


(* ******************************************************************** *)
(* Example 1                                                            *)
(*   CTL: f(x) /\ AF(Ey.g(y))                                           *)
(* ******************************************************************** *)

let ex1lab s =
  match s with
    | "f(x)" -> [(0,["x" --> "1"]); (1,["x" --> "2"])]
    | "g(y)" -> [(3,["y" --> "1"]); (4,["y" --> "2"])]
    | "f(1)" -> [(0,[])]
    | "f(2)" -> [(1,[])]
    | "g(1)" -> [(3,[])]
    | "g(2)" -> [(4,[])]
    | _ -> []
;;

let ex1graph =
  let nodes =
    [(0,"f(1)");(1,"f(2)");(2,"< >");(3,"g(1)");(4,"g(2)");(5,"<exit>")] in
  let edges = [(0,2); (1,2); (2,3); (2,4); (3,5); (4,5); (5,5)] in
  mkgraph nodes (List.map (fun (x,y) -> (x,y,())) edges)
;;

let ex1states = List.map fst (ex1graph#nodes)#tolist;;

let ex1model = (ex1graph,ex1lab,ex1states);;
let ex1model_wrapped = (ex1graph,wrap_label ex1lab,ex1states);;

let ex1s0 = Exists_("v0",Pred_ ("f(x)",UnModif "v0"));;
let ex1s1 = Exists_("v1",Pred_ ("g(y)",Modif "v1"));;
let ex1s2 = Exists_("y",ex1s1);;
let ex1s3 = AF_(ex1s2);;
let ex1s4 = And_(ex1s0,ex1s3);;

let ex1s3a = AX_(ex1s2);;
let ex1s4a = AX_(AX_(ex1s2));;
let ex1s5a = And_(ex1s0,ex1s4a);;

let ex1s0b = Pred_ ("g(y)", Modif "v0");;
let ex1s1b = Exists_ ("v0",ex1s0b);;
let ex1s2b = Exists_ ("y",ex1s1b);;
let ex1s3b = AF_(ex1s2b);;
let ex1s4b = AX_(ex1s3b);;
let ex1s5b = Pred_ ("f(x)", UnModif "v3");;
let ex1s6b = Exists_ ("v3", ex1s5b);;
let ex1s7b = Exists_ ("x", ex1s6b);;
let ex1s8b = And_(ex1s7b,ex1s4b);;

let ex1s7c = And_(ex1s6b,ex1s4b);;
let ex1s8c = Exists_("x",ex1s7c);;

let ex1phi1 = ex1s4;;
let ex1phi2 = ex1s5a;;
let ex1phi3 =
  And_
 (Exists_ ("x",
  (Exists_ ("v3",
    Pred_ ("f(x)", UnModif "v3")))),
  AX_
   (AF_
    (Exists_ ("y", (* change this to Y and have strange behaviour *)
      (Exists_ ("v0",
       Pred_ ("g(y)", Modif "v0")
                      ))))));;

let ex1phi4 =
  Exists_ ("x",
	   And_ (
	    (Exists_ ("v3",
		     Pred_ ("f(x)", UnModif "v3"))),
	    AX_
	      (AF_
		 (Exists_ ("y", (* change this to Y and have strange behaviour *)
			  (Exists_ ("v0",
				   Pred_ ("g(y)", Modif "v0")
				  )))))));;


let ex1phi5 = AU_(True_,Exists_("y", Exists_("v0",Pred_("g(y)",Modif "v0"))));;

let ex1phi6 =
  AU_(
    Not_(Exists_("x",Exists_("v1",Pred_("f(x)",UnModif "v1")))),
    Exists_("y", Exists_("v0",Pred_("g(y)",Modif "v0")))
  );;

(* use with ex1nc *)
let ex1phi7 =
  AU_(
    Not_(Or_(Pred_("f(1)",Control),Pred_("f(2)",Control))),
    Exists_("y", Exists_("v0",Pred_("g(y)",Modif "v0")))
  );;

let ex1 phi = satbis ex1model (mkanno phi);;
let ex1nc phi = satbis_noclean ex1model (mkanno phi);;


(* ******************************************************************** *)
(* Example 2                                                            *)
(* ******************************************************************** *)

let ex2lab s =
  match s with
    | "p"        -> [0,[]]
    | "{"        -> [(1,[]); (2,[])]
    | "}"        -> [(3,[]); (4,[])]
    | "paren(v)" -> [(1,["v" --> "1"]); (2,["v" --> "2"]);
		     (3,["v" --> "2"]); (4,["v" --> "1"])]
    | _          -> []
;;

let ex2graph =
  let nodes =
    [(0,"p");(1,"{");(2,"{");(3,"}");(4,"}");(5,"<exit>")] in
  let edges = [(0,1); (1,2); (2,3); (3,4); (4,5); (5,5)] in
  mkgraph nodes (List.map (fun (x,y) -> (x,y,())) edges)
;;

let ex2states = List.map fst (ex2graph#nodes)#tolist;;

let ex2model = (ex2graph,ex2lab,ex2states);;
let ex2model_wrapped = (ex2graph,wrap_label ex2lab,ex2states);;

let ex2s0 = Pred_("p",Control);;
let ex2s1 = Pred_("{",Control);;
let ex2s2 = Pred_("paren(v)",Control);;
let ex2s3 = And_(ex2s1,ex2s2);;
let ex2s4 = Pred_("}",Control);;
let ex2s5 = Pred_("paren(v)",Control);;
let ex2s6 = And_(ex2s4,ex2s5);;
let ex2s7 = AF_(ex2s6);;
let ex2s8 = And_(ex2s3,ex2s7);;
let ex2s9 = Exists_("v",ex2s8);;
let ex2s10 = AX_(ex2s9);;
let ex2s11 = And_(ex2s0,ex2s10);;

let ex2phi1 = ex2s11;;

let ex2 phi = satbis_noclean ex2model (mkanno phi)

(*
           +--- s11:& ---+
           |             |
         s0:p         s10:AX
                         |
                     s9:exists v
                         |
           +---------- s8:& --------+
           |                        |
     +-- s3:& --+                 s7:AF
     |          |                   |
   s1:"{"     s2:paren(v)     +--  s6:& -+
                              |          |
		            s4:"}"     s5:paren(v)

  s0 : p                   : (0,_,_)
  s1 : "{"                 : (1,_,_); (2,_,_)
  s2 : paren(v)            : (1,v=1,_); (2,v=2,_); (3,v=2,_); (4,v=1,_)
  s3 : "{" & paren(v)      : (1,v=1,_); (2,v=2,_)
  s4 : "}"                 : (3,_,_); (4,_,_)
  s5 : paren(v)            : (1,v=1,_); (2,v=2,_); (3,v=2,_); (4,v=1,_)
  s6 : "}" & paren(v)      : (3,v=2,_); (4,v=1,_)
  s7 : AF(...)             : (0;1;2;3,v=2,_); (0;1;2;3;4,v=1,_)
  s8 : (...&...) & AF(...) : (1,v=1,_); (2,v=2,_)
  s9 : exists ...          : (1,_,(1,v=1)); (2,_,(2,v=2))
 s10 : AX(...)             : (0,_,(1,v=1)); (1,_,(2,v=2))
 s11 : p & AX(...)         : (0,_,(1,v=1))
*)
Commit	Line	Data
9bc82bae C	1	(*
	2	* Copyright 2010, INRIA, University of Copenhagen
	3	* Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix
	4	* Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
	5	* Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
	6	* This file is part of Coccinelle.
	7	*
	8	* Coccinelle is free software: you can redistribute it and/or modify
	9	* it under the terms of the GNU General Public License as published by
	10	* the Free Software Foundation, according to version 2 of the License.
	11	*
	12	* Coccinelle is distributed in the hope that it will be useful,
	13	* but WITHOUT ANY WARRANTY; without even the implied warranty of
	14	* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
	15	* GNU General Public License for more details.
	16	*
	17	* You should have received a copy of the GNU General Public License
	18	* along with Coccinelle. If not, see <http://www.gnu.org/licenses/>.
	19	*
	20	* The authors reserve the right to distribute this or future versions of
	21	* Coccinelle under other licenses.
	22	*)
	23
	24
c491d8ee C	25	(*
	26	* Copyright 2010, INRIA, University of Copenhagen
	27	* Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix
	28	* Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
	29	* Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
	30	* This file is part of Coccinelle.
	31	*
	32	* Coccinelle is free software: you can redistribute it and/or modify
	33	* it under the terms of the GNU General Public License as published by
	34	* the Free Software Foundation, according to version 2 of the License.
	35	*
	36	* Coccinelle is distributed in the hope that it will be useful,
	37	* but WITHOUT ANY WARRANTY; without even the implied warranty of
	38	* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
	39	* GNU General Public License for more details.
	40	*
	41	* You should have received a copy of the GNU General Public License
	42	* along with Coccinelle. If not, see <http://www.gnu.org/licenses/>.
	43	*
	44	* The authors reserve the right to distribute this or future versions of
	45	* Coccinelle under other licenses.
	46	*)
	47
	48
34e49164 C	49
	50	(* ********************************************************************** *)
	51	(* Module: EXAMPLE_ENGINE (instance of CTL_ENGINE) *)
	52	(* ********************************************************************** *)
	53
	54	(* Simple env.: meta.vars and values are strings *)
	55	module SIMPLE_ENV =
	56	struct
	57	type value = string;;
	58	type mvar = string;;
	59	let eq_mvar x x' = x = x';;
	60	let eq_val v v' = v = v';;
	61	let merge_val v v' = v;;
	62	end
	63	;;
	64
	65	(* Simple predicates *)
ae4735db	66	module WRAPPER_PRED =
34e49164 C	67	struct
	68	type predicate = string
	69	end
	70
ae4735db	71	module EXAMPLE_ENGINE =
34e49164 C	72	Wrapper_ctl.CTL_ENGINE_BIS (SIMPLE_ENV) (Ctl_engine.OGRAPHEXT_GRAPH) (WRAPPER_PRED)
	73
	74	let top_wit = []
	75
	76	(* ******************************************************************** *)
	77	(* *)
	78	(* EXAMPLES *)
	79	(* *)
	80	(* ******************************************************************** *)
	81
	82	(* For convenience in the examples *)
	83	(* FIX ME: remove *)
	84	open Ctl_engine.OGRAPHEXT_GRAPH;;
	85	open EXAMPLE_ENGINE;;
	86	open Ast_ctl;;
	87
	88	(* ---------------------------------------------------------------------- *)
	89	(* Helpers *)
	90	(* ---------------------------------------------------------------------- *)
	91
	92	(* FIX ME: move to ENGINE module *)
	93	let (-->) x v = Subst (x,v);;
	94
	95	(* FIX ME: move to ENGINE module *)
	96	let (-/->) x v = NegSubst(x,v);;
	97
ae4735db	98	let mkgraph nodes edges =
34e49164	99	let g = ref (new Ograph_extended.ograph_extended) in
ae4735db C	100	let addn (n,x) =
	101	(* let (g',i) = (!g)#add_node x in *)
	102	(* now I need to force the nodei of a node, because of the state(vx) predicates
34e49164 C	103	hence add_node -> add_nodei
	104	*)
	105	let (g', i) = !g#add_nodei n x in
	106	assert (i = n);
	107	g := g'; (n,i) in
ae4735db	108	let adde anodes (n1,n2,x) =
34e49164 C	109	let g' = (!g)#add_arc ((List.assoc n1 anodes,List.assoc n2 anodes),x) in
	110	g := g'; () in
	111	let add_nodes = List.map addn nodes in
	112	let _add_edges = List.map (adde add_nodes) edges in
	113	!g
	114	;;
	115
	116
	117	(* CTL parameterised on basic predicates and metavar's*)
ae4735db	118	type ('pred,'mvar) old_gen_ctl =
34e49164 C	119	\| False_
	120	\| True_
	121	\| Pred_ of 'pred
	122	\| Not_ of ('pred,'mvar) old_gen_ctl
	123	\| Exists_ of 'mvar * ('pred,'mvar) old_gen_ctl (* !!! *)
	124	\| And_ of ('pred,'mvar) old_gen_ctl * ('pred,'mvar) old_gen_ctl
	125	\| Or_ of ('pred,'mvar) old_gen_ctl * ('pred,'mvar) old_gen_ctl
	126	\| Implies_ of ('pred,'mvar) old_gen_ctl * ('pred,'mvar) old_gen_ctl
	127	\| AF_ of ('pred,'mvar) old_gen_ctl
	128	\| AX_ of ('pred,'mvar) old_gen_ctl
	129	\| AG_ of ('pred,'mvar) old_gen_ctl
	130	\| AU_ of ('pred,'mvar) old_gen_ctl * ('pred,'mvar) old_gen_ctl
	131	\| EF_ of ('pred,'mvar) old_gen_ctl
	132	\| EX_ of ('pred,'mvar) old_gen_ctl
	133	\| EG_ of ('pred,'mvar) old_gen_ctl
	134	\| EU_ of ('pred,'mvar) old_gen_ctl * ('pred,'mvar) old_gen_ctl
	135	\| Let_ of string * ('pred,'mvar) old_gen_ctl * ('pred,'mvar) old_gen_ctl
	136	\| Ref_ of string
	137
	138	let rec mkanno phi0 =
	139	let anno phi = (phi,None) in
	140	match phi0 with
	141	\| False_ -> anno False
	142	\| True_ -> anno True
	143	\| Pred_(p) -> anno (Pred(p))
	144	\| Not_(phi) -> anno (Not(mkanno phi))
	145	\| Exists_(v,phi) -> anno (Exists(v,mkanno phi))
	146	\| And_(phi1,phi2) -> anno (And(mkanno phi1,mkanno phi2))
	147	\| Or_(phi1,phi2) -> anno (Or(mkanno phi1,mkanno phi2))
	148	\| Implies_(phi1,phi2) -> anno (Implies(mkanno phi1,mkanno phi2))
	149	\| AF_(phi1) -> anno (AF(mkanno phi1))
	150	\| AX_(phi1) -> anno (AX(mkanno phi1))
	151	\| AG_(phi1) -> anno (AG(mkanno phi1))
	152	\| AU_(phi1,phi2) -> anno (AU(mkanno phi1,mkanno phi2))
	153	\| EF_(phi1) -> anno (EF(mkanno phi1))
	154	\| EX_(phi1) -> anno (EX(mkanno phi1))
	155	\| EG_(phi1) -> anno (EG(mkanno phi1))
	156	\| EU_(phi1,phi2) -> anno (EU(mkanno phi1,mkanno phi2))
	157	\| Let_ (x,phi1,phi2) -> anno (Let(x,mkanno phi1,mkanno phi2))
	158	\| Ref_(s) -> anno (Ref(s))
	159
	160
	161	(* ******************************************************************** *)
	162	(* Example 1 *)
	163	(* CTL: f(x) /\ AF(Ey.g(y)) *)
	164	(* ******************************************************************** *)
	165
	166	let ex1lab s =
	167	match s with
	168	\| "f(x)" -> [(0,["x" --> "1"]); (1,["x" --> "2"])]
	169	\| "g(y)" -> [(3,["y" --> "1"]); (4,["y" --> "2"])]
	170	\| "f(1)" -> [(0,[])]
	171	\| "f(2)" -> [(1,[])]
	172	\| "g(1)" -> [(3,[])]
	173	\| "g(2)" -> [(4,[])]
	174	\| _ -> []
	175	;;
	176
ae4735db C	177	let ex1graph =
ae4735db C	178	let nodes =
34e49164 C	179	[(0,"f(1)");(1,"f(2)");(2,"< >");(3,"g(1)");(4,"g(2)");(5,"<exit>")] in
	180	let edges = [(0,2); (1,2); (2,3); (2,4); (3,5); (4,5); (5,5)] in
	181	mkgraph nodes (List.map (fun (x,y) -> (x,y,())) edges)
	182	;;
	183
	184	let ex1states = List.map fst (ex1graph#nodes)#tolist;;
	185
	186	let ex1model = (ex1graph,ex1lab,ex1states);;
	187	let ex1model_wrapped = (ex1graph,wrap_label ex1lab,ex1states);;
	188
	189	let ex1s0 = Exists_("v0",Pred_ ("f(x)",UnModif "v0"));;
	190	let ex1s1 = Exists_("v1",Pred_ ("g(y)",Modif "v1"));;
	191	let ex1s2 = Exists_("y",ex1s1);;
	192	let ex1s3 = AF_(ex1s2);;
	193	let ex1s4 = And_(ex1s0,ex1s3);;
	194
	195	let ex1s3a = AX_(ex1s2);;
	196	let ex1s4a = AX_(AX_(ex1s2));;
	197	let ex1s5a = And_(ex1s0,ex1s4a);;
	198
	199	let ex1s0b = Pred_ ("g(y)", Modif "v0");;
	200	let ex1s1b = Exists_ ("v0",ex1s0b);;
	201	let ex1s2b = Exists_ ("y",ex1s1b);;
	202	let ex1s3b = AF_(ex1s2b);;
	203	let ex1s4b = AX_(ex1s3b);;
	204	let ex1s5b = Pred_ ("f(x)", UnModif "v3");;
	205	let ex1s6b = Exists_ ("v3", ex1s5b);;
	206	let ex1s7b = Exists_ ("x", ex1s6b);;
	207	let ex1s8b = And_(ex1s7b,ex1s4b);;
	208
	209	let ex1s7c = And_(ex1s6b,ex1s4b);;
	210	let ex1s8c = Exists_("x",ex1s7c);;
	211
	212	let ex1phi1 = ex1s4;;
	213	let ex1phi2 = ex1s5a;;
ae4735db	214	let ex1phi3 =
34e49164 C	215	And_
	216	(Exists_ ("x",
	217	(Exists_ ("v3",
	218	Pred_ ("f(x)", UnModif "v3")))),
	219	AX_
	220	(AF_
	221	(Exists_ ("y", (* change this to Y and have strange behaviour *)
	222	(Exists_ ("v0",
	223	Pred_ ("g(y)", Modif "v0")
	224	))))));;
	225
ae4735db	226	let ex1phi4 =
34e49164 C	227	Exists_ ("x",
	228	And_ (
	229	(Exists_ ("v3",
	230	Pred_ ("f(x)", UnModif "v3"))),
	231	AX_
	232	(AF_
	233	(Exists_ ("y", (* change this to Y and have strange behaviour *)
	234	(Exists_ ("v0",
	235	Pred_ ("g(y)", Modif "v0")
	236	)))))));;
	237
	238
	239	let ex1phi5 = AU_(True_,Exists_("y", Exists_("v0",Pred_("g(y)",Modif "v0"))));;
	240
ae4735db	241	let ex1phi6 =
34e49164 C	242	AU_(
	243	Not_(Exists_("x",Exists_("v1",Pred_("f(x)",UnModif "v1")))),
	244	Exists_("y", Exists_("v0",Pred_("g(y)",Modif "v0")))
	245	);;
	246
	247	(* use with ex1nc *)
ae4735db	248	let ex1phi7 =
34e49164 C	249	AU_(
	250	Not_(Or_(Pred_("f(1)",Control),Pred_("f(2)",Control))),
	251	Exists_("y", Exists_("v0",Pred_("g(y)",Modif "v0")))
	252	);;
	253
	254	let ex1 phi = satbis ex1model (mkanno phi);;
	255	let ex1nc phi = satbis_noclean ex1model (mkanno phi);;
	256
	257
	258	(* ******************************************************************** *)
	259	(* Example 2 *)
	260	(* ******************************************************************** *)
	261
	262	let ex2lab s =
	263	match s with
	264	\| "p" -> [0,[]]
	265	\| "{" -> [(1,[]); (2,[])]
	266	\| "}" -> [(3,[]); (4,[])]
ae4735db	267	\| "paren(v)" -> [(1,["v" --> "1"]); (2,["v" --> "2"]);
34e49164 C	268	(3,["v" --> "2"]); (4,["v" --> "1"])]
	269	\| _ -> []
	270	;;
	271
ae4735db C	272	let ex2graph =
ae4735db C	273	let nodes =
34e49164 C	274	[(0,"p");(1,"{");(2,"{");(3,"}");(4,"}");(5,"<exit>")] in
	275	let edges = [(0,1); (1,2); (2,3); (3,4); (4,5); (5,5)] in
	276	mkgraph nodes (List.map (fun (x,y) -> (x,y,())) edges)
	277	;;
	278
	279	let ex2states = List.map fst (ex2graph#nodes)#tolist;;
	280
	281	let ex2model = (ex2graph,ex2lab,ex2states);;
	282	let ex2model_wrapped = (ex2graph,wrap_label ex2lab,ex2states);;
	283
	284	let ex2s0 = Pred_("p",Control);;
	285	let ex2s1 = Pred_("{",Control);;
	286	let ex2s2 = Pred_("paren(v)",Control);;
	287	let ex2s3 = And_(ex2s1,ex2s2);;
	288	let ex2s4 = Pred_("}",Control);;
	289	let ex2s5 = Pred_("paren(v)",Control);;
	290	let ex2s6 = And_(ex2s4,ex2s5);;
	291	let ex2s7 = AF_(ex2s6);;
	292	let ex2s8 = And_(ex2s3,ex2s7);;
	293	let ex2s9 = Exists_("v",ex2s8);;
	294	let ex2s10 = AX_(ex2s9);;
	295	let ex2s11 = And_(ex2s0,ex2s10);;
	296
	297	let ex2phi1 = ex2s11;;
	298
	299	let ex2 phi = satbis_noclean ex2model (mkanno phi)
	300
	301	(*
	302	+--- s11:& ---+
	303	\| \|
	304	s0:p s10:AX
	305	\|
	306	s9:exists v
	307	\|
	308	+---------- s8:& --------+
	309	\| \|
	310	+-- s3:& --+ s7:AF
	311	\| \| \|
	312	s1:"{" s2:paren(v) +-- s6:& -+
	313	\| \|
	314	s4:"}" s5:paren(v)
	315
	316	s0 : p : (0,_,_)
	317	s1 : "{" : (1,_,_); (2,_,_)
	318	s2 : paren(v) : (1,v=1,_); (2,v=2,_); (3,v=2,_); (4,v=1,_)
	319	s3 : "{" & paren(v) : (1,v=1,_); (2,v=2,_)
	320	s4 : "}" : (3,_,_); (4,_,_)
	321	s5 : paren(v) : (1,v=1,_); (2,v=2,_); (3,v=2,_); (4,v=1,_)
	322	s6 : "}" & paren(v) : (3,v=2,_); (4,v=1,_)
	323	s7 : AF(...) : (0;1;2;3,v=2,_); (0;1;2;3;4,v=1,_)
	324	s8 : (...&...) & AF(...) : (1,v=1,_); (2,v=2,_)
	325	s9 : exists ... : (1,_,(1,v=1)); (2,_,(2,v=2))
	326	s10 : AX(...) : (0,_,(1,v=1)); (1,_,(2,v=2))
	327	s11 : p & AX(...) : (0,_,(1,v=1))
	328	*)