### Profile

Statistics
| Branch: | Revision:

## cool / src / fuzzy / fuzzy.ml @ b75e5a66

 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 AF = ALCFormula ``` ```open CoolUtils ``` ```open Glpk ``` ```open FuzzyALCReasoner ``` ```let counter = ref 0 ``` ```(* 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 printUsage () = ``` ``` print_endline "Usage: \"alc []\" where"; ``` ``` print_endline " in { sat print nnf prov (is »not.(sat ¬f)«) }"; ``` ``` print_endline " in { MultiModalK MultiModalKD CoalitionLogic GML"; ``` ``` print_endline " (or: K) (or: KD) (or: CL) }"; ``` ``` 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 "Examples:"; ``` ``` print_endline " OCAMLRUNPARAM=b ./coalg sat K <<< '[R] False'"; ``` ``` print_endline " OCAMLRUNPARAM=b ./coalg sat KD <<< '[R] False'"; ``` ``` print_endline "The OCAMLRUNPARAM=b is optional. It will show a backtrace in case of a crash"; ``` ``` exit 1 ``` ```let verbose = ref false ``` ```let parseFunctor str = ``` ``` match str with ``` ``` | "K" -> CM.MultiModalK ``` ``` | "KD" -> CM.MultiModalKD ``` ``` | "CL" -> CM.CoalitionLogic ``` ``` | "GML" -> CM.GML ``` ``` | "MultiModalK" -> CM.MultiModalK ``` ``` | "MultiModalKD" -> CM.MultiModalKD ``` ``` | "CoalitionLogic" -> CM.CoalitionLogic ``` ``` | _ -> raise (CoAlgFormula.CoAlgException ("Unknown Functor name »" ^ str ^ "«")) ``` ```let choiceSat () = ``` ``` let verb = !verbose in ``` ``` let sorts = [| (parseFunctor Sys.argv.(2), [0]) |] 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 = [| (parseFunctor Sys.argv.(2), [0]) |] 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 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 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 () ``` ``` | _ -> printUsage () ``` ```*) ``` ```(* ``` ```let printUsage () = ``` ``` print_endline "Usage: \"alc []\" where"; ``` ``` print_endline " in { sat print nnf prov (is »not.(sat ¬f)«) }"; ``` ``` print_endline " in { MultiModalK MultiModalKD CoalitionLogic GML"; ``` ``` print_endline " (or: K) (or: KD) (or: CL) }"; ``` ``` 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 "Examples:"; ``` ``` print_endline " OCAMLRUNPARAM=b ./coalg sat K <<< '[R] False'"; ``` ``` print_endline " OCAMLRUNPARAM=b ./coalg sat KD <<< '[R] False'"; ``` ``` print_endline "The OCAMLRUNPARAM=b is optional. It will show a backtrace in case of a crash" ``` ```*) ``` ```let funConcat f1 f2 x = f1 (f2 x) (* XXX can't this be done better? *) ``` ```let _ = ``` ``` try ``` ``` while true do ``` ``` let input = read_line () in ``` ``` if not (GenAndComp.isEmptyString input) then ``` ``` try ( ``` ``` let in1 = FuzzyALCABox.importQuery input in ``` ``` incr counter; ``` ``` print_string ("ABox " ^ (string_of_int !counter) ^ ": "); ``` ``` let in2 = List.map (funConcat FuzzyALCABox.replaceOrForall FuzzyALCABox.collapseNeg) in1 in ``` ``` (if fuzzyALCsat in2 then ``` ``` print_endline "Satisfiable" ``` ``` else ``` ``` print_endline "Not satisfiable") ``` ``` ) with FuzzyALCABox.CoAlgException("Parsing error") -> print_endline "Parsing error" ``` ``` else () ``` ``` done ``` ``` with End_of_file -> () ```