Profile

Statistics
| Branch: | Revision:

cool / src / coalg / coalg.ml @ 9631d5b7

 1 ```(** Accepts formulae from the standard input and tests them for satisfiability. ``` ``` Each formula has to be on a separate line and empty lines are ignored. ``` ``` The input is terminated by EOF. ``` ``` @author Florian Widmann ``` ``` *) ``` ```module CM = CoAlgMisc ``` ```module CF = CoAlgFormula ``` ```module FE = FunctorParsing ``` ```open CoolUtils ``` ```(* The type of formulae that are accepted. *) ``` ```(* ``` ```let sorts = Array.make 1 (CoAlgMisc.MultiModalK, [0]) ``` ```*) ``` ```(* ``` ```let sorts = Array.make 3 (CoAlgMisc.MultiModalK, [0]) ``` ```let _ = sorts.(0) <- (CoAlgMisc.Choice, [1; 2]) ``` ```*) ``` ```(* ``` ```let sorts = [| (CoAlgMisc.MultiModalKD, [0]) ``` ``` (*; (CoAlgMisc.MultiModalKD, [1]) ``` ``` ; (CoAlgMisc.Fusion, [1; 1]) *) ``` ``` |] ``` ```let sorts = [| (CM.MultiModalK, [0]) ``` ``` (*; (CoAlgMisc.MultiModalKD, [1]) ``` ``` ; (CoAlgMisc.Fusion, [1; 1]) *) ``` ``` |] ``` ```*) ``` ```(* A partial function mapping nominals to their sorts. *) ``` ```let nomTable name = ``` ``` assert (CoAlgFormula.isNominal name); ``` ``` Some 0 ``` ```let _ = Gc.set { (Gc.get()) with Gc.minor_heap_size = 4194304; major_heap_increment = 67108864; space_overhead = 120 } ``` ```(* ``` ```let _ = ``` ``` let str = "A . B C" in ``` ``` print_endline (FE.stringFromFunctorExp (FE.functorExpFromString str)) ``` ```*) ``` ```let printUsage () = ``` ``` print_endline "Usage: \"alc []\" where"; ``` ``` print_endline " in { sat print verify nnf prov (is »not.(sat ¬f)«) nom2fix }"; ``` ``` print_endline " in { MultiModalK (or equivalently K)"; ``` ``` print_endline " MultiModalKD (or equivalently KD)"; ``` ``` print_endline " Monotone"; ``` ``` print_endline " CoalitionLogic (or equivalently CL)"; ``` ``` print_endline " Const id1 ... idn (or equivalently Constant id1 ... idn)"; ``` ``` print_endline " Id (or equivalently Identity)"; ``` ``` print_endline " PML"; ``` ``` print_endline " GML"; ``` ``` print_endline " }"; ``` ``` print_endline " where you can compose functors by:"; ``` ``` print_endline " + (weakest precedence)"; ``` ``` print_endline " or * "; ``` ``` print_endline " or . (binds strongest)"; ``` ``` print_endline " (so K+KD.CL*PML stand for (K + ((KD.CL) * PML)))"; ``` ``` print_endline " = a list of the following items"; ``` ``` print_endline " --agents AGLIST"; ``` ``` print_endline " expects the next argument AGLIST to be a list of integers"; ``` ``` print_endline " which is treaten as the set of agents for CL formulas"; ``` ``` print_endline " it defaults to 1,2,3,4,5,6,7,8,9,10"; ``` ``` print_endline " --verbose"; ``` ``` print_endline " print verbose output for sat task"; ``` ``` print_endline ""; ``` ``` print_endline "Problems are read from standard input and have the form"; ``` ``` print_endline " [ ass_1; .. ; ass_n |- ] concept"; ``` ``` print_endline "where concept, ass_1, ..., ass_n are formulae (hypothesis"; ``` ``` print_endline "and TBox assumptions) built using"; ``` ``` print_endline " True, False, ident (atomic proposition), ident' (nominal)"; ``` ``` print_endline " <=> (equivalence), => (implication), | (or), & (and), ~ (not)"; ``` ``` print_endline " @ ident' (satisfaction operator)"; ``` ``` print_endline " [R], (universal/existential restrictions along role R"; ``` ``` print_endline " [{ aglist }], <{ aglist }> (aglist can force / cannot avoid)"; ``` ``` print_endline " {<= n}, {>= n}, {< n}, {> n} (number / probability of successors)"; ``` ``` print_endline " =ident (constant value)"; ``` ``` print_endline " O (identity operator)"; ``` ``` print_endline " _ + _ (choice)"; ``` ``` print_endline " [pi1], [pi2] (fusion)"; ``` ``` print_endline ""; ``` ``` print_endline "Examples:"; ``` ``` print_endline " OCAMLRUNPARAM=b ./coalg sat K <<< '[R] False'"; ``` ``` print_endline " OCAMLRUNPARAM=b ./coalg sat KD <<< '[R] False'"; ``` ``` print_endline " OCAMLRUNPARAM=b ./coalg sat 'K + KD' <<< '(([R] False) + ([R] False))'"; ``` ``` print_endline "The OCAMLRUNPARAM=b is optional. It will show a backtrace in case of a crash"; ``` ``` exit 1 ``` ```let counter = ref 0 ``` ```let verbose = ref false ``` ```let choiceSat () = ``` ``` let verb = !verbose in ``` ``` let sorts = (FE.sortTableFromString Sys.argv.(2)) in ``` ``` let printRes sat = ``` ``` if not verb then ``` ``` print_endline (if sat then "satisfiable\n" else "unsatisfiable\n") ``` ``` else () ``` ``` in ``` ``` try ``` ``` while true do ``` ``` let input = read_line () in ``` ``` if not (GenAndComp.isEmptyString input) then ``` ``` let (tbox, f) = CoAlgFormula.importQuery input in ``` ``` incr counter; ``` ``` print_string ("\nFormula " ^ (string_of_int !counter) ^ ": "); ``` ``` flush stdout; ``` ``` printRes (CoAlgReasoner.isSat ~verbose:verb sorts nomTable tbox f) ``` ``` else () ``` ``` done ``` ``` with End_of_file -> () ``` ```let choiceProvable () = ``` ``` let verb = !verbose in ``` ``` let sorted_not ((s,f):CF.sortedFormula) : CF.sortedFormula = ``` ``` (s,CF.NOT f) ``` ``` in ``` ``` let sorts = (FE.sortTableFromString Sys.argv.(2)) in ``` ``` let printRes sat = ``` ``` if not verb then ``` ``` print_endline (if not sat then "provable\n" else "unprovable\n") ``` ``` else () ``` ``` in ``` ``` try ``` ``` while true do ``` ``` let input = read_line () in ``` ``` if not (GenAndComp.isEmptyString input) then ``` ``` let (tbox,f) = CoAlgFormula.importQuery input in ``` ``` let fneg = sorted_not f in ``` ``` incr counter; ``` ``` print_string ("\nFormula " ^ (string_of_int !counter) ^ ": "); ``` ``` flush stdout; ``` ``` printRes (CoAlgReasoner.isSat ~verbose:verb sorts nomTable tbox fneg) ``` ``` else () ``` ``` done ``` ``` with End_of_file -> () ``` ```let choicePrint () = ``` ``` try ``` ``` while true do ``` ``` let input = read_line () in ``` ``` if not (GenAndComp.isEmptyString input) then ``` ``` let f = CoAlgFormula.importFormula input in ``` ``` let str = CoAlgFormula.exportFormula f in ``` ``` incr counter; ``` ``` print_string ("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n"); ``` ``` flush stdout; ``` ``` else () ``` ``` done ``` ``` with End_of_file -> () ``` ```let choiceNom2fix () = ``` ``` try ``` ``` while true do ``` ``` let input = read_line () in ``` ``` if not (GenAndComp.isEmptyString input) then ``` ``` let f = CoAlgFormula.importFormula input in ``` ``` let str = CoAlgFormula.exportFormula f in ``` ``` incr counter; ``` ``` print_string("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n"); ``` ``` flush stdout; ``` ``` else () ``` ``` done ``` ``` with End_of_file -> () ``` ```let choiceNNF () = ``` ``` try ``` ``` while true do ``` ``` let input = read_line () in ``` ``` if not (GenAndComp.isEmptyString input) then ``` ``` let f = CoAlgFormula.nnf (CoAlgFormula.importFormula input) in ``` ``` let str = CoAlgFormula.exportFormula f in ``` ``` incr counter; ``` ``` print_string (str ^ "\n"); ``` ``` flush stdout; ``` ``` else () ``` ``` done ``` ``` with End_of_file -> () ``` ```let choiceGraph () = ``` ``` choiceSat (); ``` ``` print_endline "digraph reasonerstate {"; ``` ``` CM.graphIterCores (fun core -> print_endline (CM.coreToDot core)); ``` ``` CM.graphIterStates (fun state -> print_endline (CM.stateToDot state)); ``` ``` print_endline "}" ``` ```let choiceVerify () = ``` ``` try ``` ``` while true do ``` ``` let input = read_line () in ``` ``` if not (GenAndComp.isEmptyString input) then ``` ``` let f = CoAlgFormula.importFormula input in ``` ``` let str = CoAlgFormula.exportFormula f in ``` ``` incr counter; ``` ``` print_string ("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n"); ``` ``` flush stdout; ``` ``` CoAlgFormula.verifyFormula f; ``` ``` else () ``` ``` done ``` ``` with End_of_file -> () ``` ```let rec parseFlags arr offs : unit = ``` ``` let offs = ref (offs) in ``` ``` let getParam () = ``` ``` if ((!offs + 1) >= Array.length arr) then ``` ``` raise (CoAlgFormula.CoAlgException ("Parameter missing for flag »" ^ (arr.(!offs)) ^ "«")) ``` ``` else ``` ``` offs := !offs + 1; ``` ``` arr.(!offs) ``` ``` in ``` ``` if (!offs >= Array.length arr) then () ``` ``` else (ignore (match arr.(!offs) with ``` ``` | "--verbose" -> verbose := true ``` ``` | "--agents" -> ``` ``` let strAglist = getParam () in ``` ``` let aglist = List.map int_of_string (Str.split (Str.regexp ",") strAglist) in ``` ``` CoolUtils.cl_set_agents (Array.of_list aglist) ``` ``` | _ -> ``` ``` raise (CoAlgFormula.CoAlgException ("Unknown flag »" ^ (arr.(!offs)) ^ "«")) ``` ``` ) ; parseFlags arr (!offs + 1) ``` ``` ) ``` ```let _ = ``` ``` if Array.length Sys.argv < 3 then printUsage() ``` ``` else ``` ``` let choice = Sys.argv.(1) in ``` ``` parseFlags Sys.argv 3; ``` ``` match choice with ``` ``` | "sat" -> choiceSat () ``` ``` | "prov" -> choiceProvable () ``` ``` | "print" -> choicePrint () ``` ``` | "nnf" -> choiceNNF () ``` ``` | "verify" -> choiceVerify () ``` ``` | "graph" -> choiceGraph () ``` ``` | "nom2fix" -> choiceNom2fix() ``` ``` | _ -> printUsage () ```