### Profile

Statistics
| Branch: | Revision:

## cool / src / lib / CoAlgMisc.ml @ de84f40d

1 2 3 4fd28192 Thorsten Wißmann ```(** Common types, functions, and data structures for the CoAlgebraic reasoner. ``` ``` @author Florian Widmann ``` ``` *) ``` ```module S = MiscSolver ``` f1fa9ad5 Thorsten Wißmann ```module L = List ``` 4fd28192 Thorsten Wißmann ```module C = CoAlgFormula ``` ```module HC = HashConsing ``` ```(** An instantiation of a set (of the standard library) for bitsets. ``` ``` *) ``` ```module BsSet = Set.Make( ``` ``` struct ``` ``` type t = S.bitset ``` ``` let (compare : t -> t -> int) = S.compareBS ``` ``` end ``` ``` ) ``` ```(** An instantiation of a hash table (of the standard library) for bitsets. ``` ``` *) ``` ```module GHt = Hashtbl.Make( ``` ``` struct ``` 16af388e Christoph Egger ``` type t = S.bitset * S.bitset ``` ``` let equal ((bs1l, bs1r) : t) (bs2l, bs2r) = ``` ``` (S.compareBS bs1l bs2l = 0) && (S.compareBS bs1r bs2r = 0) ``` ``` let hash ((bsl, bsr) : t) = (S.hashBS bsl) lxor (S.hashBS bsr) ``` ``` end ``` ``` ) ``` ```(** An instantiation of a hash table (of the standard library) for bitsets. ``` ``` *) ``` ```module GHtS = Hashtbl.Make( ``` ``` struct ``` 4fd28192 Thorsten Wißmann ``` type t = S.bitset ``` ``` let equal (bs1 : t) bs2 = S.compareBS bs1 bs2 = 0 ``` ``` let hash (bs : t) = S.hashBS bs ``` ``` end ``` ``` ) ``` ```(** An instantiation of a hash table (of the standard library) for literals. ``` ``` *) ``` ```module LHt = Hashtbl.Make( ``` ``` struct ``` ``` type t = Minisat.lit ``` ``` let equal (l1 : t) l2 = l1 = l2 ``` ``` let hash (l : t) = (l :> int) ``` ``` end ``` ``` ) ``` ```(** An instantiation of a hash table (of the standard library) for formulae. ``` ``` *) ``` ```module FHt = Hashtbl.Make( ``` ``` struct ``` ``` type t = int ``` ``` let equal (f1 : t) f2 = f1 = f2 ``` ``` let hash (f : t) = f ``` ``` end ``` ``` ) ``` ```(** An instantiation of a hash table (of the standard library) for nominals. ``` ``` *) ``` ```module NHt = Hashtbl.Make( ``` ``` struct ``` ``` type t = int * int ``` ``` let equal ((s1, f1) : t) (s2, f2) = (s1 = s2) && (f1 = f2) ``` ``` let hash ((s, f) : t) = (((s+f)*(s+f+1)) / 2) + f ``` ``` end ``` ```) ``` ```(*****************************************************************************) ``` ```(* Types that can be modified rather easily *) ``` ```(* (of course you then have to modify the implementations below too) *) ``` ```(*****************************************************************************) ``` ```(* This type must be extended for additional logics. *) ``` ```type functors = ``` ``` | MultiModalK ``` a87192e8 Thorsten Wißmann ``` | MultiModalKD ``` f1fa9ad5 Thorsten Wißmann ``` | CoalitionLogic ``` 29b2e3f3 Thorsten Wißmann ``` | GML ``` 86b07be8 Thorsten Wißmann ``` | PML ``` 5e0983fe Thorsten Wißmann ``` | Constant of string list ``` 19f5dad0 Dirk Pattinson ``` | Identity ``` ``` | DefaultImplication ``` 4fd28192 Thorsten Wißmann ``` | Choice ``` ``` | Fusion ``` 5e0983fe Thorsten Wißmann ```(* functors whose constructor takes additional parameters *) ``` ```type parametricFunctorName = ``` ``` | NameConstant ``` ```(* this type should only be used in the following few helper functions *) ``` ```type functorName = ``` ``` | NPa of functors (* No Parameters = functor without parameters *) ``` ``` | Pa of parametricFunctorName (* Parameters = functor with parameters *) ``` ```let unaryfunctor2name : (functorName*string) list = ``` ``` [ (NPa MultiModalK , "MultiModalK") ``` ``` ; (NPa MultiModalKD , "MultiModalKD") ``` ``` ; (NPa GML , "GML") ``` ``` ; (NPa PML , "PML") ``` ``` ; (NPa CoalitionLogic , "CoalitionLogic") ``` ``` ; (NPa MultiModalK , "K") ``` ``` ; (NPa MultiModalKD , "KD") ``` ``` ; (NPa CoalitionLogic , "CL") ``` ``` ; (Pa NameConstant , "Const") ``` ``` ; (Pa NameConstant , "Constant") ``` 19f5dad0 Dirk Pattinson ``` ; (NPa Identity, "Id") ``` ``` ; (NPa Identity, "Identity") ``` db23edf7 Thorsten Wißmann ``` ] ``` 5e0983fe Thorsten Wißmann ```let functor2name : (functorName*string) list = ``` db23edf7 Thorsten Wißmann ``` L.append unaryfunctor2name ``` 5e0983fe Thorsten Wißmann ``` [ (NPa Choice , "Choice") ``` ``` ; (NPa Fusion , "Fusion") ``` db23edf7 Thorsten Wißmann ``` ] ``` 5e0983fe Thorsten Wißmann ```let functor_apply_parameters (func : parametricFunctorName) (params: string list) : functors option = ``` ``` (* apply parameter list to the constructor, denoted by the functor name func *) ``` ``` (* return None, if the parameters somehow don't match the required parameters *) ``` ``` match func with ``` ``` | NameConstant -> Some (Constant params) ``` ```let functor_of_string str params : functors option = ``` db23edf7 Thorsten Wißmann ``` let fst (a,b) = a in ``` ``` try ``` 5e0983fe Thorsten Wißmann ``` let functorName = fst (List.find (fun (f,name) -> name = str) functor2name) in ``` ``` match functorName with ``` ``` | NPa x -> Some x ``` ``` | Pa f -> functor_apply_parameters f params ``` db23edf7 Thorsten Wißmann ``` with Not_found -> None ``` 5e0983fe Thorsten Wißmann ```let unaryfunctor_of_string str params = ``` ``` match (functor_of_string str params) with ``` db23edf7 Thorsten Wißmann ``` | Some Choice -> None ``` ``` | Some Fusion -> None ``` ``` | x -> x ``` ```let string_of_functor (f: functors) : string = ``` 5e0983fe Thorsten Wißmann ``` (* replace f orrectly with possibly some Pa wrapper *) ``` ``` (* also put the parameters into some suffix which will be appended later *) ``` ``` let f,suffix = match f with ``` ``` | Constant params -> Pa NameConstant, " "^(String.concat " " params) ``` ``` | _ -> NPa f, "" ``` ``` in ``` db23edf7 Thorsten Wißmann ``` let snd (a,b) = b in ``` ``` try ``` 5e0983fe Thorsten Wißmann ``` let name = snd (List.find (fun (f2,name) -> f = f2) functor2name) in ``` ``` name ^ suffix ``` db23edf7 Thorsten Wißmann ``` with Not_found -> assert false ``` 4fd28192 Thorsten Wißmann ```(* This type may be extended for additional logics. *) ``` ```type formulaType = ``` ``` | Other ``` 3b055ae8 dirk ``` | TrueFalseF (* constant true or false *) ``` 4fd28192 Thorsten Wißmann ``` | AndF ``` ``` | OrF ``` ``` | AtF ``` ``` | NomF ``` 559819d7 Thorsten Wißmann ``` | ExF (* Existential / diamond *) ``` ``` | AxF (* Universal / box *) ``` 29b2e3f3 Thorsten Wißmann ``` | EnforcesF (* diamond of CL *) ``` ``` | AllowsF (* box of CL *) ``` af276a36 Thorsten Wißmann ``` | MoreThanF (* more than n successors = diamond in gml *) ``` ``` | MaxExceptF(* at most n exceptions = box in gml *) ``` 86b07be8 Thorsten Wißmann ``` | AtLeastProbF (* for PML *) ``` 9bae2c4f Thorsten Wißmann ``` | LessProbFailF (* box for PML *) ``` c49eea11 Thorsten Wißmann ``` | ConstF (* constant functor *) ``` ``` | ConstnF (* constant functor *) ``` 19f5dad0 Dirk Pattinson ``` | IdF (* Identity functor *) ``` ``` | NormF (* Default Implication *) ``` ``` | NormnF (* negation normal form of default implication *) ``` 559819d7 Thorsten Wißmann ``` | ChcF (* Choice *) ``` ``` | FusF (* Fusion *) ``` 3b407438 Christoph Egger ``` | MuF ``` ``` | NuF ``` 4fd28192 Thorsten Wißmann ```type localFormula = int ``` ```type bset = S.bitset ``` ```type atFormula = int ``` ```type cset = S.bitset ``` ```type csetSet = BsSet.t ``` ```type lht = localFormula LHt.t ``` ```type fht = Minisat.lit FHt.t ``` ```type nht = bset NHt.t ``` e0f19999 Thorsten Wißmann ```type state = { sortS : sort; ``` ``` mutable bsS : bset; (* a set of formulas who are either literals or ``` ``` modalities (TODO: also @-formulas?). ``` ``` the state is satisfiable if /\bsS is satisfiable. ``` ``` *) ``` 3285ac30 Christoph Egger ``` mutable deferralS : bset; (* which formulas still have deferrals *) ``` e0f19999 Thorsten Wißmann ``` mutable statusS : nodeStatus; ``` 4fd28192 Thorsten Wißmann ``` mutable parentsS : core list; mutable childrenS : (dependencies * core list) list; ``` 73762b19 Thorsten Wißmann ``` mutable constraintsS : csetSet; expandFkt : stateExpander; ``` ``` idx: int } ``` 4fd28192 Thorsten Wißmann e0f19999 Thorsten Wißmann ```and core = { (* for details, see documentation of newCore *) ``` ``` sortC : sort; ``` ``` mutable bsC : bset; (* a set of arbitrary formulas. ``` ``` the present core is satisfiable if /\ bsC is satisfiable *) ``` 3285ac30 Christoph Egger ``` mutable deferralC : bset; (* which formulas still have deferrals *) ``` e0f19999 Thorsten Wißmann ``` mutable statusC : nodeStatus; ``` ``` mutable parentsC : (state * int) list; ``` ``` mutable childrenC : state list; ``` ``` mutable constraintsC : csetSet; ``` ``` solver : Minisat.solver; (* a solver to find satisfying assignemnts for bsC. ``` ``` the solver returns "satisfiable" iff ``` ``` there is a satisfying assignment of ``` ``` bsC which is not represented by some state from the ``` ``` childrenC yet. ``` ``` *) ``` ``` fht : fht; (* mapping of boolean subformulas of bsC to their corresponding literals ``` ``` of the Minisat solver ``` ``` *) ``` 73762b19 Thorsten Wißmann ``` mutable constraintParents : cset list; ``` ``` idx : int } ``` 4fd28192 Thorsten Wißmann d283bf7a Thorsten Wißmann ```and setState = state GHt.t array ``` 4fd28192 Thorsten Wißmann d283bf7a Thorsten Wißmann ```and setCore = core GHt.t array ``` 4fd28192 Thorsten Wißmann 16af388e Christoph Egger ```and setCnstr = unit GHtS.t ``` 4fd28192 Thorsten Wißmann ```(*****************************************************************************) ``` ```(* Types that are hard coded into the algorithm *) ``` ```(*****************************************************************************) ``` 269d93e5 Thorsten Wißmann ```and 'a junction = | Disjunctive of 'a (*specifies that any of the 'a needs to be satifsfied *) ``` ``` | Conjunctive of 'a (*specifies that all of the 'a need to be satifsfied *) ``` a9949a25 Thorsten Wißmann ```and stateExpander = rule lazylist ``` 4fd28192 Thorsten Wißmann ```and sort = C.sort ``` ```and nodeStatus = ``` ``` | Expandable ``` ``` | Open ``` ``` | Sat ``` ``` | Unsat ``` f4498ed1 Christoph Egger ```(* In K, given the singleton list [bs] returns the list of all Ax'es ``` ``` responsible for the individual members of bs being part of the core ``` ``` as well as the Ex. ``` ``` So given the state { <>φ , []ψ , []η } and the core { φ , ψ , η }, ``` ``` dependency would map { η } to { <>φ , []η } and { ψ } to { <>φ , []ψ } ``` ```*) ``` 4fd28192 Thorsten Wißmann ```and dependencies = bset list -> bset ``` 269d93e5 Thorsten Wißmann f4498ed1 Christoph Egger ```(* Note: sort * bset * bset is to be read as sort * formulas_in_core * deferrals_in_core *) ``` 16af388e Christoph Egger ```and rule = (dependencies * (sort * bset * bset) lazylist) ``` 269d93e5 Thorsten Wißmann a9949a25 Thorsten Wißmann ```and 'a lazyliststep = ``` 69243f7f Thorsten Wißmann ``` | MultipleElements of 'a list ``` ``` | SingleElement of 'a ``` ``` | NoMoreElements ``` a9949a25 Thorsten Wißmann ```and 'a lazylist = unit -> 'a lazyliststep ``` ```and ruleEnumeration = rule lazyliststep ``` f335015f Thorsten Wißmann ```let nodeStatusToString : nodeStatus -> string = function ``` ``` | Expandable -> "Expandable" ``` ``` | Open -> "Open" ``` ``` | Sat -> "Sat" ``` ``` | Unsat -> "Unsat" ``` a9949a25 Thorsten Wißmann ```let lazylistFromList a_list = ``` ``` let list_state = ref (Some a_list) in ``` ``` fun () -> begin match !list_state with ``` ``` | Some (a_list) -> begin ``` ``` list_state := None; ``` ``` MultipleElements a_list ``` ``` end ``` ``` | None -> NoMoreElements ``` ``` end ``` 4fd28192 Thorsten Wißmann 672429b4 Thorsten Wißmann ```let rec listFromLazylist evalfunc = ``` ``` let step = evalfunc () in ``` ``` match step with ``` ``` | NoMoreElements -> [] ``` ``` | SingleElement x -> x::(listFromLazylist evalfunc) ``` ``` | MultipleElements xs -> List.append xs (listFromLazylist evalfunc) ``` 4fd28192 Thorsten Wißmann ```type nominal = sort * localFormula ``` ```type node = ``` ``` | State of state ``` ``` | Core of core ``` ```type constrnt = ``` ``` | UnsatC ``` ``` | SatC ``` ``` | OpenC of node list ``` ``` | UnexpandedC of node list ``` ```type propagateElement = ``` ``` | UState of state * int option ``` ``` | UCore of core * bool ``` ``` | UCnstr of cset ``` ```type queueElement = ``` ``` | QState of state ``` ``` | QCore of core ``` ``` | QCnstr of cset ``` ``` | QEmpty ``` ```type sortTable = (functors * int list) array ``` ```exception CoAlg_finished of bool ``` ```let sortTable = ref (Array.make 0 (MultiModalK, [1])) ``` 269d93e5 Thorsten Wißmann ```let junctionEvalBool : (bool list junction) -> bool = function ``` ``` | Disjunctive l -> List.fold_right (||) l false ``` ``` | Conjunctive l -> List.fold_right (&&) l true ``` ```let junctionEval (f: 'a -> bool) : 'a list junction -> bool = function ``` ``` | Disjunctive l -> List.fold_right (fun x y -> (f x) || y) l false ``` ``` | Conjunctive l -> List.fold_right (fun x y -> (f x) && y) l true ``` ```let optionalizeOperator (f: 'a -> 'b -> 'c) (x: 'a option) (y: 'b option) : 'c option = ``` ``` match x with ``` ``` | None -> None ``` ``` | Some x -> (match y with ``` ``` | None -> None ``` ``` | Some y -> Some (f x y)) ``` ```let junctionEvalBoolOption : bool option list junction -> bool option = ``` ``` let f extreme op x y = (* ensure that: (Some True) || None = Some True *) ``` ``` if x = extreme || y = extreme ``` ``` then extreme ``` ``` else optionalizeOperator op x y ``` ``` in function ``` ``` | Disjunctive l -> ``` ``` List.fold_right (f (Some true) (||)) l (Some false) ``` ``` | Conjunctive l -> ``` ``` List.fold_right (f (Some false) (&&)) l (Some true) ``` ```let junctionExtract : 'a junction -> ('a * ('b -> 'b junction)) = function ``` ``` | Disjunctive l -> (l, fun x -> Disjunctive x) ``` ``` | Conjunctive l -> (l, fun x -> Conjunctive x) ``` 4fd28192 Thorsten Wißmann ```(*****************************************************************************) ``` ```(* "Module type" and a specific implementation of the main queue *) ``` ```(*****************************************************************************) ``` ```let queueStates = ref ([] : state list) ``` ```let queueCores1 = ref ([] : core list) ``` ```let queueCores2 = ref ([] : core list) ``` ```let queueCnstrs = ref ([] : cset list) ``` ```let doPropagation = ref false ``` ```let queueInit () = ``` ``` queueStates := []; ``` ``` queueCores1 := []; ``` ``` queueCores2 := []; ``` ``` queueCnstrs := []; ``` ``` doPropagation := false ``` ```let queueIsEmpty () = ``` ``` !queueStates = [] && !queueCores1 = [] && !queueCores2 = [] && !queueCnstrs = [] ``` ```let queueInsertState state = queueStates := state::!queueStates ``` d58bba0f Dirk Pattinson ```(* original version: breadth-first *) ``` 4fd28192 Thorsten Wißmann ```let queueInsertCore core = queueCores2 := core::!queueCores2 ``` 034a8dea Christoph Egger ```(* experiment: depth first ``` d58bba0f Dirk Pattinson ```let queueInsertCore core = queueCores1 := core::!queueCores1 ``` ```*) ``` 4fd28192 Thorsten Wißmann ```let queueInsertCnstr cset = queueCnstrs := cset::!queueCnstrs ``` ```let queueGetElement () = ``` ``` if !queueCnstrs <> [] then ``` ``` let res = List.hd !queueCnstrs in ``` ``` queueCnstrs := List.tl !queueCnstrs; ``` ``` QCnstr res ``` ``` else if !queueStates <> [] then ``` ``` let res = List.hd !queueStates in ``` ``` queueStates := List.tl !queueStates; ``` ``` QState res ``` ``` else if !queueCores1 <> [] then ``` ``` let res = List.hd !queueCores1 in ``` ``` queueCores1 := List.tl !queueCores1; ``` ``` QCore res ``` ``` else if !queueCores2 = [] then QEmpty ``` ``` else ``` ``` let res = List.hd !queueCores2 in ``` ``` doPropagation := true; ``` ``` queueCores1 := List.tl !queueCores2; ``` ``` queueCores2 := []; ``` ``` QCore res ``` ```let doNominalPropagation () = !doPropagation ``` ```let doSatPropagation () = ``` ``` let res = !doPropagation in ``` ``` doPropagation := false; ``` ``` res ``` ```(*****************************************************************************) ``` ```(* "Module type" and a specific implementation of the graph *) ``` ```(*****************************************************************************) ``` ```let graphStates = ref (Array.make 0 (GHt.create 0 : state GHt.t)) ``` ```let graphCores = ref (Array.make 0 (GHt.create 0 : core GHt.t)) ``` 16af388e Christoph Egger ```let graphCnstrs = ref (GHtS.create 0 : constrnt GHtS.t) ``` 4fd28192 Thorsten Wißmann ```let graphRoot = ref (None : core option) ``` ```let graphInit () = ``` ``` let size = Array.length !sortTable in ``` ``` graphStates := Array.init size (fun _ -> GHt.create 128); ``` ``` graphCores := Array.init size (fun _ -> GHt.create 128); ``` 16af388e Christoph Egger ``` graphCnstrs := GHtS.create 128; ``` 4fd28192 Thorsten Wißmann ``` graphRoot := None ``` ```let graphIterStates fkt = ``` ``` Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) !graphStates ``` ```let graphIterCores fkt = ``` ``` Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) !graphCores ``` 16af388e Christoph Egger ```let graphIterCnstrs fkt = GHtS.iter fkt !graphCnstrs ``` 4fd28192 Thorsten Wißmann ```let graphClearCnstr () = ``` 16af388e Christoph Egger ``` let newGraph = GHtS.create (GHtS.length !graphCnstrs) in ``` 4fd28192 Thorsten Wißmann ``` let copyCnstr cset cnstr = ``` ``` match cnstr with ``` ``` | UnsatC ``` 16af388e Christoph Egger ``` | SatC -> GHtS.add newGraph cset cnstr ``` ``` | OpenC _ -> GHtS.add newGraph cset (OpenC []) ``` ``` | UnexpandedC _ -> GHtS.add newGraph cset (UnexpandedC []) ``` 4fd28192 Thorsten Wißmann ``` in ``` 16af388e Christoph Egger ``` GHtS.iter copyCnstr !graphCnstrs; ``` 4fd28192 Thorsten Wißmann ``` graphCnstrs := newGraph ``` ```let graphFindState sort bs = ``` ``` try ``` ``` Some (GHt.find !graphStates.(sort) bs) ``` ``` with Not_found -> None ``` ```let graphFindCore sort bs = ``` ``` try ``` ``` Some (GHt.find !graphCores.(sort) bs) ``` ``` with Not_found -> None ``` ```let graphFindCnstr cset = ``` ``` try ``` 16af388e Christoph Egger ``` Some (GHtS.find !graphCnstrs cset) ``` 4fd28192 Thorsten Wißmann ``` with Not_found -> None ``` ```let graphInsertState sort bs state = ``` ``` assert (not (GHt.mem !graphStates.(sort) bs)); ``` ``` GHt.add !graphStates.(sort) bs state ``` ```let graphInsertCore sort bs core = ``` ``` assert (not (GHt.mem !graphCores.(sort) bs)); ``` ``` GHt.add !graphCores.(sort) bs core ``` ```let graphInsertCnstr cset cnstr = ``` 16af388e Christoph Egger ``` assert (not (GHtS.mem !graphCnstrs cset)); ``` ``` GHtS.add !graphCnstrs cset cnstr ``` 4fd28192 Thorsten Wißmann ```let graphReplaceCnstr cset cnstr = ``` 16af388e Christoph Egger ``` GHtS.replace !graphCnstrs cset cnstr ``` 4fd28192 Thorsten Wißmann ```let graphSizeState () = ``` ``` Array.fold_left (fun acc ht -> acc + GHt.length ht) 0 !graphStates ``` ```let graphSizeCore () = ``` ``` Array.fold_left (fun acc ht -> acc + GHt.length ht) 0 !graphCores ``` 16af388e Christoph Egger ```let graphSizeCnstr () = GHtS.length !graphCnstrs ``` 4fd28192 Thorsten Wißmann ```let graphAddRoot core = ``` ``` if !graphRoot = None then graphRoot := Some core ``` ``` else raise (C.CoAlgException "Root of graph is already set.") ``` ```let graphGetRoot () = ``` ``` match !graphRoot with ``` ``` | None -> raise (C.CoAlgException "Root of graph is not set.") ``` ``` | Some core -> core ``` ```(*****************************************************************************) ``` ```(* "Module type" and a specific implementation of sets of constraints *) ``` ```(*****************************************************************************) ``` ```let cssEmpty = BsSet.empty ``` ```let cssExists fkt css = BsSet.exists fkt css ``` ```let cssForall fkt css = BsSet.for_all fkt css ``` ```let cssUnion css1 css2 = BsSet.union css1 css2 ``` ```let cssAdd cset css = BsSet.add cset css ``` ```let cssFold fkt css init = BsSet.fold fkt css init ``` ```let cssSingleton cset = BsSet.singleton cset ``` ```let cssEqual css1 css2 = BsSet.equal css1 css2 ``` f335015f Thorsten Wißmann ```let cssIter (action: cset -> unit) css = ``` ``` BsSet.iter action css ``` 4fd28192 Thorsten Wißmann ```(*****************************************************************************) ``` ```(* "Module type" and a specific implementation of state nodes *) ``` ```(*****************************************************************************) ``` 73762b19 Thorsten Wißmann ```let nodeCounter = ref 0 ``` ```let nextNodeIdx () : int = ``` ``` let oldVal = !nodeCounter in ``` ``` nodeCounter := oldVal + 1; ``` ``` oldVal ``` 3285ac30 Christoph Egger ```let stateMake sort bs defer exp = ``` ``` { sortS = sort; bsS = bs; deferralS = defer; statusS = Expandable; parentsS = []; childrenS = []; ``` 73762b19 Thorsten Wißmann ``` constraintsS = cssEmpty; expandFkt = exp; ``` ``` idx = nextNodeIdx() ``` ``` } ``` 4fd28192 Thorsten Wißmann ```let stateGetSort state = state.sortS ``` ```let stateGetBs state = state.bsS ``` ```let stateSetBs state bs = state.bsS <- bs ``` 3285ac30 Christoph Egger ```let stateGetDeferral state = state.deferralS ``` ```let stateSetDeferral state bs = state.deferralS <- bs ``` 4fd28192 Thorsten Wißmann ```let stateGetStatus state = state.statusS ``` ```let stateSetStatus state status = state.statusS <- status ``` ```let stateGetParents state = state.parentsS ``` ```let stateAddParent state parent = state.parentsS <- parent::state.parentsS ``` ```let stateGetRule state idx = List.nth state.childrenS (List.length state.childrenS - idx) ``` ```let stateGetRules state = state.childrenS ``` ```let stateAddRule state dep children = ``` ``` state.childrenS <- (dep, children)::state.childrenS; ``` ``` List.length state.childrenS ``` ```let stateGetConstraints state = state.constraintsS ``` ```let stateSetConstraints state csets = state.constraintsS <- csets ``` ```let stateNextRule state = state.expandFkt () ``` 73762b19 Thorsten Wißmann ```let stateGetIdx (state:state) = state.idx ``` 4fd28192 Thorsten Wißmann ```(*****************************************************************************) ``` ```(* "Module type" and a specific implementation of core nodes *) ``` ```(*****************************************************************************) ``` 3285ac30 Christoph Egger ```let coreMake sort bs defer solver fht = ``` ``` { sortC = sort; bsC = bs; deferralC = defer; statusC = Expandable; parentsC = []; childrenC = []; ``` 73762b19 Thorsten Wißmann ``` constraintsC = cssEmpty; solver = solver; fht = fht; constraintParents = []; ``` ``` idx = nextNodeIdx() ``` ``` } ``` 4fd28192 Thorsten Wißmann ```let coreGetSort core = core.sortC ``` ```let coreGetBs core = core.bsC ``` ```let coreSetBs core bs = core.bsC <- bs ``` 3285ac30 Christoph Egger ```let coreGetDeferral core = core.deferralC ``` ```let coreSetDeferral core bs = core.deferralC <- bs ``` 4fd28192 Thorsten Wißmann ```let coreGetStatus core = core.statusC ``` ```let coreSetStatus core status = core.statusC <- status ``` ```let coreGetParents core = core.parentsC ``` ```let coreAddParent core parent idx = core.parentsC <- (parent, idx)::core.parentsC ``` ```let coreGetChildren core = core.childrenC ``` ```let coreAddChild core child = core.childrenC <- child::core.childrenC ``` ```let coreGetConstraints core = core.constraintsC ``` ```let coreSetConstraints core csets = core.constraintsC <- csets ``` ```let coreGetSolver core = core.solver ``` ```let coreGetFht core = core.fht ``` 73762b19 Thorsten Wißmann ```let coreGetIdx (core:core) = core.idx ``` 4fd28192 Thorsten Wißmann ```let coreGetConstraintParents core = core.constraintParents ``` ```let coreAddConstraintParent core cset = ``` ``` core.constraintParents <- cset::core.constraintParents ``` ```(*****************************************************************************) ``` ```(* "Module type" and a specific implementation of sets of *) ``` ```(* states, cores, and constraints for the sat propagation *) ``` ```(*****************************************************************************) ``` d283bf7a Thorsten Wißmann ```let setEmptyState () = Array.init (Array.length !sortTable) (fun _ -> GHt.create 128) ``` ```let setEmptyCore () = Array.init (Array.length !sortTable) (fun _ -> GHt.create 128) ``` 16af388e Christoph Egger ```let setEmptyCnstr () = GHtS.create 128 ``` ```let setAddState set state = ``` ``` GHt.add set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state)) state ``` ```let setAddCore set core = ``` ``` GHt.add set.(coreGetSort core) ((coreGetBs core), (coreGetDeferral core)) core ``` ```let setAddCnstr set cset = GHtS.add set cset () ``` ```let setMemState set state = ``` ``` GHt.mem set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state)) ``` ```let setMemCore set core = ``` ``` GHt.mem set.(coreGetSort core) ((coreGetBs core), (coreGetDeferral core)) ``` ```let setMemCnstr set cset = GHtS.mem set cset ``` ```let setRemoveState set state = ``` ``` GHt.remove set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state)) ``` ```let setRemoveCore set core = ``` ``` GHt.remove set.(coreGetSort core) ((coreGetBs core), (coreGetDeferral core)) ``` ```let setRemoveCnstr set cset = GHtS.remove set cset ``` d283bf7a Thorsten Wißmann ```let setIterState fkt set = Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) set ``` ```let setIterCore fkt set = Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) set ``` 16af388e Christoph Egger ```let setIterCnstr fkt set = GHtS.iter (fun cset () -> fkt cset) set ``` 50df1dc2 Christoph Egger ```let setLengthState seta = Array.fold_left (fun acc set -> acc + GHt.length set) 0 seta ``` ```let setLengthCore seta = Array.fold_left (fun acc set -> acc + GHt.length set) 0 seta ``` 4fd28192 Thorsten Wißmann ```(*****************************************************************************) ``` ```(* "Module type" and a specific implementation of the mapping *) ``` ```(* between (local) formulae and literals of the sat solver, *) ``` ```(* and of a mapping of nominals to sets of formulae *) ``` ```(*****************************************************************************) ``` ```let lhtInit () = LHt.create 16 ``` ```let lhtAdd lht lit f = LHt.add lht lit f ``` ```let lhtFind lht lit = ``` ``` try ``` ``` Some (LHt.find lht lit) ``` ``` with Not_found -> None ``` ```let fhtInit () = FHt.create 16 ``` ```let fhtAdd fht f lit = FHt.add fht f lit ``` ```let fhtFind fht f = ``` ``` try ``` ``` Some (FHt.find fht f) ``` ``` with Not_found -> None ``` ```let nhtInit () = NHt.create 8 ``` ```let nhtAdd nht nom bs = NHt.add nht nom bs ``` ```let nhtFind nht nom = ``` ``` try ``` ``` Some (NHt.find nht nom) ``` ``` with Not_found -> None ``` ```let nhtFold fkt nht init = NHt.fold fkt nht init ``` ```(*****************************************************************************) ``` ```(* "Module type" and a specific implementation of sets of *) ``` ```(* local formulae and @-formulae *) ``` ```(*****************************************************************************) ``` ```let tboxTable = ref (Array.make 0 S.dummyBS) ``` ```let bsetMake () = S.makeBS () ``` ```let bsetAdd bs lf = S.addBSNoChk bs lf ``` ```let bsetMem bs lf = S.memBS bs lf ``` b7445f7e Thorsten Wißmann ```let bsetRem bs lf = S.remBS bs lf ``` 16af388e Christoph Egger ```let bsetCompare bs1 bs2 = S.compareBS bs1 bs2 ``` 45d554b0 Thorsten Wißmann ```let bsetMakeRealEmpty () = ``` ``` let res = bsetMake () in ``` ``` bsetRem res !S.bstrue; (* remove bstrue which is initially in an empty bset *) ``` ``` res ``` b7c3a47e Thorsten Wißmann ```let bsetCopy bs = S.copyBS bs ``` 4fd28192 Thorsten Wißmann ```let bsetFold fkt bs init = S.foldBS fkt bs init ``` ```let bsetIter fkt bset = S.iterBS fkt bset ``` e4cd869a Thorsten Wißmann ```let bsetFilter (a: bset) (f: localFormula -> bool) : bset = ``` 45d554b0 Thorsten Wißmann ``` let res = bsetMakeRealEmpty () in ``` e4cd869a Thorsten Wißmann ``` bsetIter (fun form -> if (f form) then bsetAdd res form else ()) a; ``` ``` res ``` 4fd28192 Thorsten Wißmann ```let bsetAddTBox sort bs = S.unionBSNoChk bs !tboxTable.(sort) ``` ```let csetCompare cs1 cs2 = S.compareBS cs1 cs2 ``` ```let csetMake () = S.makeBS () ``` ```let csetAdd cs lf = S.addBSNoChk cs lf ``` ```let csetCopy cs = S.copyBS cs ``` ```let csetUnion cs1 cs2 = S.unionBSNoChk cs1 cs2 ``` ```let csetHasDot cs = S.memBS cs !S.bsfalse ``` ```let csetAddDot cs = S.addBSNoChk cs !S.bsfalse ``` ```let csetRemDot cs = S.remBS cs !S.bsfalse ``` ```let csetAddTBox sort cs = S.unionBSNoChk cs !tboxTable.(sort) ``` ```let csetIter cs fkt = ``` ``` let fkt2 f = if not (f = !S.bstrue || f = !S.bsfalse) then fkt f else () in ``` ``` S.iterBS fkt2 cs ``` ```(*****************************************************************************) ``` ```(* "Module type" and a specific implementation of *) ``` ```(* local formulae and @-formulae *) ``` ```(*****************************************************************************) ``` ```(** This table maps integers (representing formulae) to their corresponding formulae. ``` ``` *) ``` ```let arrayFormula = ref (Array.make 0 (Array.make 0 C.TRUE)) ``` ```(** This table maps integers (representing formulae) to their corresponding type. ``` ``` *) ``` ```let arrayType = ref (Array.make 0 (Array.make 0 Other)) ``` ```(** This lookup table maps formulae (represented as integers) ``` ``` to their negation (in negation normal form). ``` ``` *) ``` ```let arrayNeg = ref (Array.make 0 (Array.make 0 (-1))) ``` ```(** These lookup tables map formulae (represented as integers) ``` ``` to their decompositions (represented as integers). ``` ``` This is done according to the rules of the tableau procedure ``` ``` and depends on the type of the formulae. ``` ``` *) ``` 86b07be8 Thorsten Wißmann ``` (* ``` ``` for PML: arrayDest1 = the subformula ``` eda515b6 Thorsten Wißmann ``` arrayNum = the nominator of the probability ``` ``` arrayNum2 = the denominator of the probability ``` 86b07be8 Thorsten Wißmann ``` *) ``` f1fa9ad5 Thorsten Wißmann ```let arrayDest1 = ref (Array.make 0 (Array.make 0 (-1))) (* first subformula *) ``` ```let arrayDest2 = ref (Array.make 0 (Array.make 0 (-1))) (* second subformula *) ``` ```let arrayDest3 = ref (Array.make 0 (Array.make 0 (-1))) (* a role *) ``` d9f4e4af Christoph Egger ```let arrayDeferral = ref (Array.make 0 (Array.make 0 (-1))) (* deferral at point *) ``` 29b2e3f3 Thorsten Wißmann ```let arrayDestNum = ref (Array.make 0 (Array.make 0 (-1))) (* an integer *) ``` eda515b6 Thorsten Wißmann ```let arrayDestNum2 = ref (Array.make 0 (Array.make 0 (-1))) (* another integer *) ``` f1fa9ad5 Thorsten Wißmann ```let arrayDestAg = ref (Array.make 0 (Array.make 0 [|0|])) (* arrays of agents *) ``` 4fd28192 Thorsten Wißmann ```(** This lookup table maps formulae (represented as integers) ``` ``` to their @-wrapper. ``` ``` *) ``` ```let arrayAt = ref (Array.make 0 (Array.make 0 (FHt.create 64))) ``` ```let lfGetType sort f = !arrayType.(sort).(f) ``` ```let lfGetDest1 sort f = !arrayDest1.(sort).(f) ``` ```let lfGetDest2 sort f = !arrayDest2.(sort).(f) ``` ```let lfGetDest3 sort f = !arrayDest3.(sort).(f) ``` c67aca42 Christoph Egger ```let lfGetDeferral sort f = !arrayDeferral.(sort).(f) ``` 29b2e3f3 Thorsten Wißmann ```let lfGetDestNum sort f = !arrayDestNum.(sort).(f) ``` eda515b6 Thorsten Wißmann ```let lfGetDestNum2 sort f = !arrayDestNum2.(sort).(f) ``` f1fa9ad5 Thorsten Wißmann ```let lfGetDestAg sort f = !arrayDestAg.(sort).(f) ``` 4fd28192 Thorsten Wißmann ```let lfGetNeg sort f = ``` ``` let nf = !arrayNeg.(sort).(f) in ``` ``` if nf >= 0 then Some nf else None ``` ```let lfGetAt (sort, nom) f = ``` ``` FHt.find !arrayAt.(sort).(f) nom ``` a0cffef0 Thorsten Wißmann ```let lfToInt lf = lf ``` ```let lfFromInt num = num ``` f335015f Thorsten Wißmann ```let lfGetFormula sort f = !arrayFormula.(sort).(f) ``` de84f40d Christoph Egger ```let escapeHtml (input : string) : string = ``` ``` List.fold_right (fun (x, y) (str : string) -> Str.global_replace (Str.regexp x) y str) ``` ``` [("<", "<") ; (">", ">") ; ("&", "&")] ``` ``` input ``` f335015f Thorsten Wißmann ```let bsetToString sort bset : string = ``` ``` let toFormula (lf:localFormula) (lst: string list) : string list = ``` ``` let formula: C.formula = lfGetFormula sort lf in ``` ``` (C.string_of_formula formula) :: lst ``` ``` in ``` ``` let formulaList = bsetFold toFormula bset [] in ``` ``` "{ "^(String.concat ", " formulaList)^" }" ``` ```let csetToString sort cset = bsetToString sort cset ``` 8d6bf016 Christoph Egger ```let coreToString (core:core): string = ``` f335015f Thorsten Wißmann ``` let helper cset lst : string list = ``` ``` (csetToString core.sortC cset):: lst ``` ``` in ``` ``` let constraints = cssFold helper core.constraintsC [] in ``` 488cea0f Thorsten Wißmann ``` let children = ``` ``` List.map (fun (st:state) -> string_of_int st.idx) core.childrenC ``` ``` in ``` 4164c8e1 Thorsten Wißmann ``` let parents = ``` ``` List.map (fun (st,_:state*int) -> string_of_int st.idx) core.parentsC ``` ``` in ``` 73762b19 Thorsten Wißmann ``` "Core "^(string_of_int core.idx)^" {\n"^ ``` f335015f Thorsten Wißmann ``` " Status: " ^ (nodeStatusToString core.statusC) ^ "\n"^ ``` ``` " " ^ bsetToString core.sortC core.bsC ^ "\n" ^ ``` 16af388e Christoph Egger ``` " Deferrals: \n" ^ ``` ``` " " ^ bsetToString core.sortC core.deferralC ^ "\n" ^ ``` 73762b19 Thorsten Wißmann ``` " Constraints: { "^(String.concat ``` ``` "\n " constraints)^" }\n"^ ``` 488cea0f Thorsten Wißmann ``` " Children: { "^(String.concat ``` ``` ", " children)^" }\n"^ ``` 4164c8e1 Thorsten Wißmann ``` " Parents: { "^(String.concat ", " parents)^" }\n"^ ``` f335015f Thorsten Wißmann ``` "}" ``` 73762b19 Thorsten Wißmann ```let stateToString (state:state): string = ``` ``` let helper cset lst : string list = ``` ``` (csetToString state.sortS cset):: lst ``` ``` in ``` ``` let constraints = cssFold helper state.constraintsS [] in ``` ``` let core2idx core = core.idx in ``` ``` let fst (a,b) = a in ``` ``` let conclusionList = ``` ``` List.map (fun (_,lst) -> ``` ``` List.map (fun (core:core) -> string_of_int core.idx) lst ``` ``` ) state.childrenS ``` ``` in ``` ``` let conclusionList = ``` ``` List.map (fun x -> "{"^String.concat ", " x^"}") conclusionList ``` ``` in ``` 4164c8e1 Thorsten Wißmann ``` let parents = ``` ``` List.map (fun (co:core) -> string_of_int co.idx) state.parentsS ``` ``` in ``` 73762b19 Thorsten Wißmann ``` "State "^(string_of_int state.idx)^" {\n"^ ``` ``` " Status: " ^ (nodeStatusToString state.statusS) ^ "\n"^ ``` ``` " " ^ bsetToString state.sortS state.bsS ^ "\n" ^ ``` 16af388e Christoph Egger ``` " Deferrals: \n" ^ ``` ``` " " ^ bsetToString state.sortS state.deferralS ^ "\n" ^ ``` 73762b19 Thorsten Wißmann ``` " Constraints: { "^(String.concat ``` ``` "\n " constraints)^" }\n"^ ``` ``` " Children: { "^(String.concat ``` ``` "\n " conclusionList)^" }\n"^ ``` 4164c8e1 Thorsten Wißmann ``` " Parents: { "^(String.concat ", " parents)^" }\n"^ ``` 73762b19 Thorsten Wißmann ``` "}" ``` 8d6bf016 Christoph Egger ```let stateToDot (state:state): string = ``` c13029a3 Christoph Egger ``` let color = match state.statusS with ``` ``` | Sat -> "green" ``` ``` | Unsat -> "red" ``` ``` | Open -> "yellow" ``` ``` | Expandable -> "white" ``` ``` in ``` de84f40d Christoph Egger ``` let toFormula (lf:localFormula) (lst: string list) : string list = ``` ``` let formula: C.formula = lfGetFormula state.sortS lf in ``` ``` if (bsetMem state.deferralS lf) ``` ``` then (""^(escapeHtml (C.string_of_formula formula))^"") :: lst ``` ``` else (escapeHtml (C.string_of_formula formula)) :: lst ``` ``` in ``` ``` let formulaList = bsetFold toFormula state.bsS [] in ``` 8d6bf016 Christoph Egger ``` let ownidx = (string_of_int state.idx) in ``` ``` let parents = ``` c13029a3 Christoph Egger ``` List.map (fun (co:core) -> ``` ``` "Node"^string_of_int co.idx^" -> Node"^ownidx^";") ``` 8d6bf016 Christoph Egger ``` state.parentsS ``` ``` in ``` c13029a3 Christoph Egger ``` "Node" ^ ownidx ^ " [shape=ellipse,style=filled,fillcolor=" ^ color ``` de84f40d Christoph Egger ``` ^ ",label=" ^ (String.concat "
" formulaList) ``` ``` ^ ">];\n" ``` 8d6bf016 Christoph Egger ``` ^ (String.concat "\n" parents) ``` ```let coreToDot (core:core): string = ``` c13029a3 Christoph Egger ``` let color = match core.statusC with ``` ``` | Sat -> "green" ``` ``` | Unsat -> "red" ``` ``` | Open -> "yellow" ``` ``` | Expandable -> "white" ``` ``` in ``` de84f40d Christoph Egger ``` let toFormula (lf:localFormula) (lst: string list) : string list = ``` ``` let formula: C.formula = lfGetFormula core.sortC lf in ``` ``` if (bsetMem core.deferralC lf) ``` ``` then (""^(escapeHtml (C.string_of_formula formula))^"") :: lst ``` ``` else (escapeHtml (C.string_of_formula formula)) :: lst ``` ``` in ``` ``` let formulaList = bsetFold toFormula core.bsC [] in ``` 8d6bf016 Christoph Egger ``` let ownidx = (string_of_int core.idx) in ``` ``` let parents = ``` c13029a3 Christoph Egger ``` List.map (fun (st,_:state*int) -> ``` ``` "Node"^string_of_int st.idx^" -> Node"^ownidx^";") ``` 8d6bf016 Christoph Egger ``` core.parentsC ``` ``` in ``` c13029a3 Christoph Egger ``` "Node" ^ ownidx ^ " [shape=ellipse,style=filled,fillcolor=" ^ color ``` de84f40d Christoph Egger ``` ^ ",label=" ^ (String.concat "
" formulaList) ``` ``` ^ ">];\n" ``` 8d6bf016 Christoph Egger ``` ^ (String.concat "\n" parents) ``` 488cea0f Thorsten Wißmann ```let queuePrettyStatus () = ``` ``` let printList (sl : int list) : string = ``` ``` String.concat ", " (List.map string_of_int sl) ``` ``` in ``` ``` (* TODO: are atFormulas always look-up-able for sort 0? *) ``` ``` (Printf.sprintf "%d Constraints: " (List.length !queueCnstrs)) ``` ``` ^(String.concat ", " (List.map (csetToString 0) !queueCnstrs)) ``` ``` ^(Printf.sprintf "\n%d States: " (List.length !queueStates)) ``` ``` ^(printList (List.map (fun (st:state) -> st.idx) !queueStates)) ``` ``` ^(Printf.sprintf "\n%d Cores1: " (List.length !queueCores1)) ``` ``` ^(printList (List.map (fun (co:core) -> co.idx) !queueCores1)) ``` ``` ^(Printf.sprintf "\n%d Cores2: " (List.length !queueCores2)) ``` ``` ^(printList (List.map (fun (co:core) -> co.idx) !queueCores2)) ``` ``` ^"\n" ``` 73762b19 Thorsten Wißmann 4fd28192 Thorsten Wißmann ```let atFormulaGetSubformula f = !arrayDest1.(0).(f) ``` ```let atFormulaGetNominal f = ``` ``` let s = !arrayDest3.(0).(f) in ``` ``` let n = !arrayDest2.(0).(f) in ``` ``` (s, n) ``` ```let lfToAt _ lf = lf ``` 4b0d0388 Christoph Egger ```(* Calculate all possible formulae. This includes all subformulae and ``` ``` in the case of μ-Calculus the Fischer-Ladner closure. ``` 4fd28192 Thorsten Wißmann 4b0d0388 Christoph Egger ``` TODO: variable sort needs to match epected sort ``` ``` *) ``` cb12f8a5 Christoph Egger ```let rec detClosure vars nomTbl hcF fset vset atset nomset s f = ``` ``` let newvars = List.filter (fun (x) -> C.hc_freeIn x f) vars in ``` ``` let detClosure_ = detClosure newvars in ``` ``` let deferral = if List.length newvars > 0 ``` ``` then (List.hd newvars) ``` ``` else "ε" in ``` 4fd28192 Thorsten Wißmann ``` if s < 0 || s >= Array.length fset then ``` ``` let sstr = string_of_int s in ``` ``` raise (C.CoAlgException ("Invalid sort (i.e. sort out of range): " ^ sstr)) ``` ``` else (); ``` 653eaa4b Christoph Egger ``` if C.HcFHt.mem vset.(s) f && ``` ``` compare (C.HcFHt.find vset.(s) f) deferral = 0 then () ``` 4fd28192 Thorsten Wißmann ``` else ``` cb12f8a5 Christoph Egger ``` let () = C.HcFHt.add vset.(s) f deferral in ``` 4fd28192 Thorsten Wißmann ``` let () = C.HcFHt.add fset.(s) f () in ``` ``` let (func, sortlst) = !sortTable.(s) in ``` ``` match f.HC.node with ``` ``` | C.HCTRUE ``` 43194ed2 Christoph Egger ``` | C.HCFALSE ``` ``` | C.HCVAR _ -> () ``` 4fd28192 Thorsten Wißmann ``` | C.HCAP name -> ``` ``` if C.isNominal name then begin ``` ``` Hashtbl.replace nomset name s; ``` ``` match nomTbl name with ``` ``` | None -> raise (C.CoAlgException ("Unknown nominal: " ^ name)) ``` ``` | Some sort -> ``` ``` if sort <> s then ``` ``` let str1 = "Nominal: " ^ name ^ " of sort " ^ (string_of_int sort) in ``` ``` let str2 = " is used in sort " ^ (string_of_int s) ^ "." in ``` ``` raise (C.CoAlgException (str1 ^ str2)) ``` ``` else () ``` ``` end else () ``` ``` | C.HCNOT _ -> () ``` ``` | C.HCAT (name, f1) -> ``` ``` C.HcFHt.replace atset f (); ``` ``` let s1 = ``` ``` match nomTbl name with ``` ``` | None -> raise (C.CoAlgException ("Unknown nominal: " ^ name)) ``` ``` | Some sort -> sort ``` ``` in ``` ``` let hcnom = C.HcFormula.hashcons hcF (C.HCAP name) in ``` cb12f8a5 Christoph Egger ``` detClosure_ nomTbl hcF fset vset atset nomset s1 hcnom; ``` ``` detClosure_ nomTbl hcF fset vset atset nomset s1 f1 ``` 4fd28192 Thorsten Wißmann ``` | C.HCOR (f1, f2) ``` ``` | C.HCAND (f1, f2) -> ``` cb12f8a5 Christoph Egger ``` detClosure_ nomTbl hcF fset vset atset nomset s f1; ``` ``` detClosure_ nomTbl hcF fset vset atset nomset s f2 ``` 4fd28192 Thorsten Wißmann ``` | C.HCEX (_, f1) ``` ``` | C.HCAX (_, f1) -> ``` 2a84977e Thorsten Wißmann ``` if (func <> MultiModalK && func <> MultiModalKD) ``` ``` || List.length sortlst <> 1 ``` ``` then raise (C.CoAlgException "Ex/Ax-formula is used in wrong sort.") ``` 4fd28192 Thorsten Wißmann ``` else (); ``` cb12f8a5 Christoph Egger ``` detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1 ``` f1fa9ad5 Thorsten Wißmann ``` | C.HCENFORCES (_, f1) ``` ``` | C.HCALLOWS (_, f1) -> ``` ``` if func <> CoalitionLogic || List.length sortlst <> 1 ``` ``` then raise (C.CoAlgException "[{Agents}]-formula is used in wrong sort.") ``` ``` else (); ``` cb12f8a5 Christoph Egger ``` detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1 ``` af276a36 Thorsten Wißmann ``` | C.HCMORETHAN (_,_,f1) ``` ``` | C.HCMAXEXCEPT (_,_,f1) -> ``` 29b2e3f3 Thorsten Wißmann ``` if func <> GML || List.length sortlst <> 1 ``` ``` then raise (C.CoAlgException "[{>=,<=}]-formula is used in wrong sort.") ``` ``` else (); ``` cb12f8a5 Christoph Egger ``` detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1 ``` 86b07be8 Thorsten Wißmann ``` | C.HCATLEASTPROB (_,f1) ``` 9bae2c4f Thorsten Wißmann ``` | C.HCLESSPROBFAIL (_,f1) -> ``` 86b07be8 Thorsten Wißmann ``` if func <> PML || List.length sortlst <> 1 ``` c855ba91 Thorsten Wißmann ``` then raise (C.CoAlgException "[{>=,<}]-formula with probability is used in wrong sort.") ``` 86b07be8 Thorsten Wißmann ``` else (); ``` cb12f8a5 Christoph Egger ``` detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1; ``` 9bae2c4f Thorsten Wißmann ``` (* ``` ``` TODO: add ¬ f1 to the closure! ``` ``` detClosure nomTbl hcF fset atset nomset (List.hd sortlst) (f1.HC.node.negNde) ``` ``` *) ``` 5e0983fe Thorsten Wißmann ``` | C.HCCONST color ``` ``` | C.HCCONSTN color -> ``` ``` begin match func with ``` ``` | Constant params -> ``` ``` if not (List.exists ((=) color) params) ``` ``` then raise (C.CoAlgException ("=-formula mentions \""^color^"\" but the only" ``` ``` ^" choices are: "^(String.concat ", " params))) ``` ``` | _ -> raise (C.CoAlgException "=-formula is used in wrong sort.") ``` ``` end; ``` ``` if List.length sortlst <> 1 ``` c49eea11 Thorsten Wißmann ``` then raise (C.CoAlgException "=-formula is used in wrong sort.") ``` ``` else (); ``` ``` (* NB: =-formulae have no subformlae hence no closure *) ``` 19f5dad0 Dirk Pattinson ``` | C.HCID f1 -> ``` ``` if func <> Identity || List.length sortlst <> 1 ``` ``` then raise (C.CoAlgException "Identity operator applied to ``` ``` formula of wrong sort.") ``` ``` else (); ``` cb12f8a5 Christoph Egger ``` detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1; ``` 19f5dad0 Dirk Pattinson ``` | C.HCNORM (f1, f2) ``` ``` | C.HCNORMN(f1, f2) -> ``` ``` if func <> DefaultImplication || List.length sortlst <> 1 then ``` ``` raise (C.CoAlgException "Default Implication applied to ``` ``` formulae of wrong sort.") ``` ``` else (); ``` cb12f8a5 Christoph Egger ``` detClosure_ nomTbl hcF fset vset atset nomset (List.nth sortlst 0) f1; ``` ``` detClosure_ nomTbl hcF fset vset atset nomset (List.nth sortlst 1) f2 ``` 19f5dad0 Dirk Pattinson d58bba0f Dirk Pattinson ``` | C.HCCHC (f1, f2) -> ``` 4fd28192 Thorsten Wißmann ``` if func <> Choice || List.length sortlst <> 2 then ``` ``` raise (C.CoAlgException "Choice formula is used in wrong sort.") ``` ``` else (); ``` cb12f8a5 Christoph Egger ``` detClosure_ nomTbl hcF fset vset atset nomset (List.nth sortlst 0) f1; ``` ``` detClosure_ nomTbl hcF fset vset atset nomset (List.nth sortlst 1) f2 ``` 4fd28192 Thorsten Wißmann ``` | C.HCFUS (first, f1) -> ``` ``` if func <> Fusion || List.length sortlst <> 2 then ``` ``` raise (C.CoAlgException "Fusion formula is used in wrong sort.") ``` ``` else (); ``` ``` let s1 = List.nth sortlst (if first then 0 else 1) in ``` cb12f8a5 Christoph Egger ``` detClosure_ nomTbl hcF fset vset atset nomset s1 f1 ``` 034a8dea Christoph Egger ``` (* ``` 6553983f Christoph Egger ``` FL(μ X . φ) = {μ X . φ} ∪ FL(φ[X|->μ X . φ]) ``` 034a8dea Christoph Egger ``` *) ``` ``` | C.HCMU (name, f1) -> ``` cb12f8a5 Christoph Egger ``` let () = C.HcFHt.replace vset.(s) f name in ``` 034a8dea Christoph Egger ``` let unfold = C.hc_replace hcF name f f1 in ``` cb12f8a5 Christoph Egger ``` let appendvars = List.append newvars [name] in ``` ``` detClosure appendvars nomTbl hcF fset vset atset nomset s unfold ``` 034a8dea Christoph Egger ``` | C.HCNU (name, f1) -> ``` ``` let unfold = C.hc_replace hcF name f f1 in ``` cb12f8a5 Christoph Egger ``` detClosure_ nomTbl hcF fset vset atset nomset s unfold ``` 6553983f Christoph Egger 4fd28192 Thorsten Wißmann ```let detClosureAt hcF atset name f () = ``` ``` match f.HC.node with ``` ``` | C.HCTRUE ``` ``` | C.HCFALSE ``` ``` | C.HCOR _ ``` ``` | C.HCAND _ ``` ``` | C.HCAT _ -> () ``` ``` | _ -> ``` 034a8dea Christoph Egger ``` let at = C.HcFormula.hashcons hcF (C.HCAT (name, f)) in ``` 4fd28192 Thorsten Wißmann ``` C.HcFHt.replace atset at () ``` ```(** Initialises the arrays for a formula and its integer representation. ``` ``` *) ``` d9f4e4af Christoph Egger ```let initTables nomTbl hcF htF htR vset s f n = ``` 4fd28192 Thorsten Wißmann ``` !arrayFormula.(s).(n) <- f.HC.fml; ``` d9f4e4af Christoph Egger ``` !arrayDeferral.(s).(n) <- Hashtbl.hash (C.HcFHt.find vset.(s) f); ``` 4fd28192 Thorsten Wißmann ``` let fneg = f.HC.neg in ``` ``` if C.HcFHt.mem htF.(s) fneg then !arrayNeg.(s).(n) <- C.HcFHt.find htF.(s) fneg; ``` ``` let (_, sortlst) = !sortTable.(s) in ``` ``` match f.HC.node with ``` ``` | C.HCTRUE ``` 3b055ae8 dirk ``` | C.HCFALSE -> !arrayType.(s).(n) <- TrueFalseF ``` 4fd28192 Thorsten Wißmann ``` | C.HCAP name -> ``` ``` if C.isNominal name then !arrayType.(s).(n) <- NomF ``` ``` else !arrayType.(s).(n) <- Other ``` ``` | C.HCNOT _ -> !arrayType.(s).(n) <- Other ``` ``` | C.HCAT (name, f1) -> ``` ``` !arrayType.(s).(n) <- AtF; ``` ``` let s1 = ``` ``` match nomTbl name with ``` ``` | None -> assert false ``` ``` | Some sort -> sort ``` ``` in ``` ``` let hcnom = C.HcFormula.hashcons hcF (C.HCAP name) in ``` ``` !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s1) f1; ``` ``` !arrayDest2.(s).(n) <- C.HcFHt.find htF.(s1) hcnom; ``` ``` !arrayDest3.(s).(n) <- s1 ``` ``` | C.HCOR (f1, f2) -> ``` ``` !arrayType.(s).(n) <- OrF; ``` ``` !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) f1; ``` ``` !arrayDest2.(s).(n) <- C.HcFHt.find htF.(s) f2 ``` ``` | C.HCAND (f1, f2) -> ``` ``` !arrayType.(s).(n) <- AndF; ``` ``` !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) f1; ``` ``` !arrayDest2.(s).(n) <- C.HcFHt.find htF.(s) f2 ``` 034a8dea Christoph Egger ``` | C.HCEX (role, f1) -> ``` 4fd28192 Thorsten Wißmann ``` !arrayType.(s).(n) <- ExF; ``` ``` !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1; ``` 034a8dea Christoph Egger ``` !arrayDest3.(s).(n) <- ``` 4fd28192 Thorsten Wißmann ``` if Hashtbl.mem htR role then Hashtbl.find htR role ``` ``` else ``` ``` let size = Hashtbl.length htR in ``` ``` Hashtbl.add htR role size; ``` ``` size ``` ``` | C.HCAX (role, f1) -> ``` ``` !arrayType.(s).(n) <- AxF; ``` ``` !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1; ``` ``` !arrayDest3.(s).(n) <- ``` ``` if Hashtbl.mem htR role then Hashtbl.find htR role ``` ``` else ``` ``` let size = Hashtbl.length htR in ``` ``` Hashtbl.add htR role size; ``` ``` size ``` f1fa9ad5 Thorsten Wißmann ``` | C.HCENFORCES (aglist, f1) -> (* aglist = list of agents *) ``` ``` !arrayType.(s).(n) <- EnforcesF; ``` ``` !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1; ``` ``` !arrayDestAg.(s).(n) <- Array.of_list aglist ``` ``` | C.HCALLOWS (aglist, f1) -> (* aglist = list of agents *) ``` ``` !arrayType.(s).(n) <- AllowsF; ``` ``` !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1; ``` ``` !arrayDestAg.(s).(n) <- Array.of_list aglist ``` af276a36 Thorsten Wißmann ``` | C.HCMORETHAN (cnt,role,f1) -> ``` ``` !arrayType.(s).(n) <- MoreThanF; ``` 29b2e3f3 Thorsten Wißmann ``` !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1; ``` ``` !arrayDestNum.(s).(n) <- cnt; ``` ``` !arrayDest3.(s).(n) <- ``` ``` if Hashtbl.mem htR role then Hashtbl.find htR role ``` ``` else ``` ``` let size = Hashtbl.length htR in ``` ``` Hashtbl.add htR role size; ``` ``` size ``` af276a36 Thorsten Wißmann ``` | C.HCMAXEXCEPT (cnt,role,f1) -> ``` ``` !arrayType.(s).(n) <- MaxExceptF; ``` 29b2e3f3 Thorsten Wißmann ``` !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1; ``` ``` !arrayDestNum.(s).(n) <- cnt; ``` ``` !arrayDest3.(s).(n) <- ``` ``` if Hashtbl.mem htR role then Hashtbl.find htR role ``` ``` else ``` ``` let size = Hashtbl.length htR in ``` ``` Hashtbl.add htR role size; ``` ``` size ``` 86b07be8 Thorsten Wißmann ``` | C.HCATLEASTPROB (p,f1) -> ``` ``` !arrayType.(s).(n) <- AtLeastProbF; ``` ``` !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1; ``` eda515b6 Thorsten Wißmann ``` !arrayDestNum.(s).(n) <- p.C.nominator; ``` ``` !arrayDestNum2.(s).(n) <- p.C.denominator ``` 9bae2c4f Thorsten Wißmann ``` | C.HCLESSPROBFAIL (p,f1) -> ``` ``` !arrayType.(s).(n) <- LessProbFailF; ``` 86b07be8 Thorsten Wißmann ``` !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1; ``` eda515b6 Thorsten Wißmann ``` !arrayDestNum.(s).(n) <- p.C.nominator; ``` ``` !arrayDestNum2.(s).(n) <- p.C.denominator ``` c49eea11 Thorsten Wißmann ``` | 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 *) ``` 19f5dad0 Dirk Pattinson ``` | C.HCID (f1) -> ``` ``` !arrayType.(s).(n) <- IdF; ``` d58bba0f Dirk Pattinson ``` !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 0) f1 ``` 034a8dea Christoph Egger ``` | C.HCNORM (f1, f2) -> ``` 19f5dad0 Dirk Pattinson ``` !arrayType.(s).(n) <- NormF; ``` ``` !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 0) f1; ``` ``` !arrayDest2.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 1) f2 ``` 034a8dea Christoph Egger ``` | C.HCNORMN (f1, f2) -> ``` 19f5dad0 Dirk Pattinson ``` !arrayType.(s).(n) <- NormnF; ``` ``` !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 0) f1; ``` ``` !arrayDest2.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 1) f2 ``` ``` (* note that choice is self-dual *) ``` d58bba0f Dirk Pattinson ``` | C.HCCHC (f1, f2) -> ``` 4fd28192 Thorsten Wißmann ``` !arrayType.(s).(n) <- ChcF; ``` ``` !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 0) f1; ``` ``` !arrayDest2.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 1) f2 ``` ``` | C.HCFUS (first, f1) -> ``` ``` !arrayType.(s).(n) <- FusF; ``` ``` let s1 = List.nth sortlst (if first then 0 else 1) in ``` ``` !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s1) f1; ``` ``` !arrayDest3.(s).(n) <- if first then 0 else 1 ``` 5ec97220 Christoph Egger ``` | C.HCMU (name, f1) -> ``` ``` !arrayType.(s).(n) <- MuF; ``` 034a8dea Christoph Egger ``` let unfold = C.hc_replace hcF name f f1 in ``` ``` !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) unfold ``` 5ec97220 Christoph Egger ``` | C.HCNU (name, f1) -> ``` 034a8dea Christoph Egger ``` !arrayType.(s).(n) <- NuF; ``` ``` let unfold = C.hc_replace hcF name f f1 in ``` ``` !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) unfold ``` 5ec97220 Christoph Egger ``` | C.HCVAR _ -> !arrayType.(s).(n) <- Other ``` 4fd28192 Thorsten Wißmann ```let initTablesAt hcF htF name sort = ``` ``` let hcnom = C.HcFormula.hashcons hcF (C.HCAP name) in ``` ``` let nom = C.HcFHt.find htF.(sort) hcnom in ``` ``` let addAt f n = ``` ``` match f.HC.node with ``` ``` | C.HCTRUE ``` ``` | C.HCFALSE ``` ``` | C.HCOR _ ``` ``` | C.HCAND _ ``` ``` | C.HCAT _ -> () ``` ``` | _ -> ``` 034a8dea Christoph Egger ``` let at = C.HcFormula.hashcons hcF (C.HCAT (name, f)) in ``` 4fd28192 Thorsten Wißmann ``` let atn = C.HcFHt.find htF.(0) at in ``` ``` FHt.add !arrayAt.(sort).(n) nom atn ``` ``` in ``` ``` C.HcFHt.iter addAt htF.(sort) ``` ```let ppFormulae nomTbl tbox (s, f) = ``` ``` let card = Array.length !sortTable in ``` ``` if card <= 0 then ``` ``` raise (C.CoAlgException "Number of sorts must be positive.") ``` ``` else (); ``` ``` let nnfAndSimplify f = C.simplify (C.nnf f) in ``` f828ad2f Thorsten Wißmann ``` let f1 = nnfAndSimplify f in ``` ``` let nf1 = nnfAndSimplify (C.NOT f) in ``` ``` let tbox1 = List.map (fun (s, f) -> (s, nnfAndSimplify f)) tbox in ``` ``` let ntbox1 = List.map (fun (s, f) -> (s, nnfAndSimplify (C.NOT f))) tbox in ``` ``` let hcF = C.HcFormula.create true in ``` ``` let hcf = C.hc_formula hcF f1 in ``` ``` let nhcf = C.hc_formula hcF nf1 in ``` ``` let hctbox = List.map (fun (s, f) -> (s, C.hc_formula hcF f)) tbox1 in ``` ``` let nhctbox = List.map (fun (s, f) -> (s, C.hc_formula hcF f)) ntbox1 in ``` 4fd28192 Thorsten Wißmann ``` let hcfalse = C.hc_formula hcF C.FALSE in ``` f828ad2f Thorsten Wißmann ``` let hctrue = C.hc_formula hcF C.TRUE in ``` 4fd28192 Thorsten Wißmann ``` let fset = Array.init card (fun _ -> C.HcFHt.create 128) in ``` cb12f8a5 Christoph Egger ``` let vset = Array.init card (fun _ -> C.HcFHt.create 128) in ``` 4fd28192 Thorsten Wißmann ``` let atset = C.HcFHt.create 64 in ``` ``` let nomset = Hashtbl.create 16 in ``` ``` for i = 0 to card-1 do ``` cb12f8a5 Christoph Egger ``` detClosure [] nomTbl hcF fset vset atset nomset i hcfalse; ``` ``` detClosure [] nomTbl hcF fset vset atset nomset i hctrue; ``` 4fd28192 Thorsten Wißmann ``` done; ``` cb12f8a5 Christoph Egger ``` detClosure [] nomTbl hcF fset vset atset nomset s hcf; ``` ``` detClosure [] nomTbl hcF fset vset atset nomset s nhcf; ``` ``` List.iter (fun (s, f) -> detClosure [] nomTbl hcF fset vset atset nomset s f) ``` ``` hctbox; ``` ``` List.iter (fun (s, f) -> detClosure [] nomTbl hcF fset vset atset nomset s f) ``` ``` nhctbox; ``` 4fd28192 Thorsten Wißmann ``` Hashtbl.iter (fun n s -> C.HcFHt.iter (detClosureAt hcF atset n) fset.(s)) nomset; ``` ``` let htF = Array.init card (fun _ -> C.HcFHt.create 128) in ``` ``` for i = 0 to card-1 do ``` ``` C.HcFHt.add htF.(i) hcfalse 0; ``` ``` C.HcFHt.add htF.(i) hctrue 1 ``` ``` done; ``` ``` let addAts f () idx = ``` ``` for i = 0 to card-1 do ``` ``` C.HcFHt.add htF.(i) f idx ``` ``` done; ``` ``` idx + 1 ``` ``` in ``` ``` let sizeAt = C.HcFHt.fold addAts atset 2 in ``` ``` let addFml i f () idx = ``` ``` if C.HcFHt.mem htF.(i) f then idx ``` ``` else begin ``` ``` C.HcFHt.add htF.(i) f idx; ``` ``` idx+1 ``` ``` end ``` ``` in ``` ``` let size = ref 0 in ``` ``` for i = 0 to card-1 do ``` ``` let size2 = C.HcFHt.fold (addFml i) fset.(i) sizeAt in ``` ``` if size2 > !size then size := size2 else () ``` ``` done; ``` ``` arrayFormula := Array.init card (fun _ -> Array.make !size C.TRUE); ``` ``` arrayType := Array.init card (fun _ -> Array.make !size Other); ``` ``` arrayDest1 := Array.init card (fun _ -> Array.make !size (-1)); ``` ``` arrayDest2 := Array.init card (fun _ -> Array.make !size (-1)); ``` ``` arrayDest3 := Array.init card (fun _ -> Array.make !size (-1)); ``` d9f4e4af Christoph Egger ``` arrayDeferral := Array.init card (fun _-> Array.make !size(-1)); ``` 4fd28192 Thorsten Wißmann ``` arrayNeg := Array.init card (fun _ -> Array.make !size (-1)); ``` 29b2e3f3 Thorsten Wißmann ``` arrayDestNum := Array.init card (fun _ -> Array.make !size (-1)); ``` eda515b6 Thorsten Wißmann ``` arrayDestNum2 := Array.init card (fun _ -> Array.make !size (-1)); ``` 98af95fb Thorsten Wißmann ``` arrayDestAg := Array.init card (fun _ -> Array.make !size (Array.make 0 (-1))); ``` 4fd28192 Thorsten Wißmann ``` let htR = Hashtbl.create 128 in ``` d9f4e4af Christoph Egger ``` Array.iteri (fun s ht -> C.HcFHt.iter (initTables nomTbl hcF htF htR vset s) ht) htF; ``` 4fd28192 Thorsten Wißmann ``` arrayAt := Array.init card (fun _ -> Array.init !size (fun _ -> FHt.create 8)); ``` ``` Hashtbl.iter (initTablesAt hcF htF) nomset; ``` ``` S.initMisc !size (C.HcFHt.find htF.(0) hcfalse) (C.HcFHt.find htF.(0) hctrue) (-1) (-1) (-1); ``` ``` let initbs = bsetMake () in ``` ``` bsetAdd initbs (C.HcFHt.find htF.(s) hcf); ``` ``` let tboxTbl = Array.init card (fun _ -> bsetMake ()) in ``` ``` List.iter (fun (s, f) -> bsetAdd tboxTbl.(s) (C.HcFHt.find htF.(s) f)) hctbox; ``` ``` tboxTable := tboxTbl; ``` ` (tbox1, (s, f1), initbs)`