Project

General

Profile

Statistics
| Branch: | Revision:

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

History | View | Annotate | Download (8.57 KB)

1
(** Accepts formulae from the standard input and tests them for satisfiability.
2
    Each formula has to be on a separate line and empty lines are ignored.
3
    The input is terminated by EOF.
4
    @author Florian Widmann
5
 *)
6

    
7
module CM = CoAlgMisc
8
module CF = CoAlgFormula
9

    
10
module FE = FunctorParsing
11

    
12
open CoolUtils
13

    
14
(* The type of formulae that are accepted. *)
15
(*
16
let sorts = Array.make 1 (CoAlgMisc.MultiModalK, [0])
17
*)
18
(*
19
let sorts = Array.make 3 (CoAlgMisc.MultiModalK, [0])
20
let _ = sorts.(0) <- (CoAlgMisc.Choice, [1; 2])
21
*)
22
(*
23
let sorts = [| (CoAlgMisc.MultiModalKD, [0])
24
            (*;  (CoAlgMisc.MultiModalKD, [1])
25
            ;  (CoAlgMisc.Fusion, [1; 1]) *)
26
            |]
27
let sorts = [| (CM.MultiModalK, [0])
28
            (*;  (CoAlgMisc.MultiModalKD, [1])
29
            ;  (CoAlgMisc.Fusion, [1; 1]) *)
30
            |]
31
*)
32

    
33
(* A partial function mapping nominals to their sorts. *)
34
let nomTable name =
35
  assert (CoAlgFormula.isNominal name);
36
  Some 0
37

    
38

    
39
let _ = Gc.set { (Gc.get()) with Gc.minor_heap_size = 4194304; major_heap_increment = 67108864; space_overhead = 120 }
40

    
41
(*
42
let _ =
43
    let str = "A . B C" in
44
    print_endline (FE.stringFromFunctorExp (FE.functorExpFromString str))
45
*)
46

    
47
let printUsage () =
48
  print_endline "Usage: \"alc <task> <functor> [<flags>]\" where";
49
  print_endline "       <task> in { sat print verify nnf prov (is »not.(sat ¬f)«) nom2fix }";
50
  print_endline "       <functor> in { MultiModalK (or equivalently K)";
51
  print_endline "                      MultiModalKD (or equivalently KD)";
52
  print_endline "                      Monotone";
53
  print_endline "                      CoalitionLogic (or equivalently CL)";
54
  print_endline "                      Const id1 ... idn (or equivalently Constant id1 ... idn)";
55
  print_endline "                      Id (or equivalently Identity)";
56
  print_endline "                      PML";
57
  print_endline "                      GML";
58
  print_endline "                    }";
59
  print_endline "                 where you can compose functors by:";
60
  print_endline "                    <functor> + <functor> (weakest precedence)";
61
  print_endline "                 or <functor> * <functor>";
62
  print_endline "                 or <functor> . <functor> (binds strongest)";
63
  print_endline "                 (so K+KD.CL*PML stand for (K + ((KD.CL) * PML)))";
64
  print_endline "       <flags> = a list of the following items";
65
  print_endline "           --agents AGLIST";
66
  print_endline "             expects the next argument AGLIST to be a list of integers";
67
  print_endline "             which is treaten as the set of agents for CL formulas";
68
  print_endline "             it defaults to 1,2,3,4,5,6,7,8,9,10";
69
  print_endline "           --verbose";
70
  print_endline "             print verbose output for sat task";
71
  print_endline "";
72
  print_endline "Problems are read from standard input and have the form";
73
  print_endline "       [ ass_1; .. ; ass_n |- ] concept";
74
  print_endline "where concept, ass_1, ..., ass_n are formulae (hypothesis";
75
  print_endline "and TBox assumptions) built using";
76
  print_endline "    True, False, ident (atomic proposition), ident' (nominal)";
77
  print_endline "    <=> (equivalence), => (implication), | (or), & (and), ~ (not)";
78
  print_endline "    @ ident' (satisfaction operator)";
79
  print_endline "    [R], <R> (universal/existential restrictions along role R";
80
  print_endline "    [{ aglist }], <{ aglist }> (aglist can force / cannot avoid)";
81
  print_endline "    {<= n}, {>= n}, {< n}, {> n} (number / probability of successors)";
82
  print_endline "    =ident (constant value)";
83
  print_endline "    O (identity operator)";
84
  print_endline "    _ + _ (choice)";
85
  print_endline "    [pi1], [pi2] (fusion)";
86
  print_endline "";
87
  print_endline "Examples:";
88
  print_endline "  OCAMLRUNPARAM=b ./coalg sat K <<< '[R] False'";
89
  print_endline "  OCAMLRUNPARAM=b ./coalg sat KD <<< '[R] False'";
90
  print_endline "  OCAMLRUNPARAM=b ./coalg sat 'K + KD' <<< '(([R] False) + ([R] False))'";
91
  print_endline "The OCAMLRUNPARAM=b is optional. It will show a backtrace in case of a crash";
92
  exit 1
93

    
94
let counter = ref 0
95
let verbose = ref false
96

    
97
let choiceSat () =
98
    let verb = !verbose in
99
    let sorts = (FE.sortTableFromString Sys.argv.(2)) in
100
    let printRes sat =
101
      if not verb then
102
        print_endline (if sat then "satisfiable\n" else "unsatisfiable\n")
103
      else ()
104
    in
105
    try
106
      while true do
107
        let input = read_line () in
108
        if not (GenAndComp.isEmptyString input) then
109
          let (tbox, f) = CoAlgFormula.importQuery input in
110
          incr counter;
111
          print_string ("\nFormula " ^ (string_of_int !counter) ^ ": ");
112
          flush stdout;
113
          printRes (CoAlgReasoner.isSat ~verbose:verb sorts nomTable tbox f)
114
        else ()
115
      done
116
    with End_of_file -> ()
117

    
118
let choiceProvable () =
119
    let verb = !verbose in
120
    let sorted_not ((s,f):CF.sortedFormula) : CF.sortedFormula =
121
        (s,CF.NOT f)
122
    in
123
    let sorts = (FE.sortTableFromString Sys.argv.(2)) in
124
    let printRes sat =
125
      if not verb then
126
        print_endline (if not sat then "provable\n" else "unprovable\n")
127
      else ()
128
    in
129
    try
130
      while true do
131
        let input = read_line () in
132
        if not (GenAndComp.isEmptyString input) then
133
          let (tbox,f) = CoAlgFormula.importQuery input in
134
          let fneg = sorted_not f in
135
          incr counter;
136
          print_string ("\nFormula " ^ (string_of_int !counter) ^ ": ");
137
          flush stdout;
138
          printRes (CoAlgReasoner.isSat ~verbose:verb sorts nomTable tbox fneg)
139
        else ()
140
      done
141
    with End_of_file -> ()
142

    
143
let choicePrint () =
144
    try
145
      while true do
146
        let input = read_line () in
147
        if not (GenAndComp.isEmptyString input) then
148
          let f = CoAlgFormula.importFormula input in
149
          let str = CoAlgFormula.exportFormula f in
150
          incr counter;
151
          print_string ("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
152
          flush stdout;
153
        else ()
154
      done
155
    with End_of_file -> ()
156

    
157
let choiceNom2fix () =
158
	try
159
		while true do
160
			let input = read_line () in
161
			if not (GenAndComp.isEmptyString input) then
162
				let f = CoAlgFormula.importFormula input in
163
				let str = CoAlgFormula.exportFormula f in
164
				incr counter;
165
				print_string("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
166
				flush stdout;
167
			else ()
168
		done
169
	with End_of_file -> ()
170

    
171
let choiceNNF () =
172
    try
173
      while true do
174
        let input = read_line () in
175
        if not (GenAndComp.isEmptyString input) then
176
          let f = CoAlgFormula.nnf (CoAlgFormula.importFormula input) in
177
          let str = CoAlgFormula.exportFormula f in
178
          incr counter;
179
          print_string (str ^ "\n");
180
          flush stdout;
181
        else ()
182
      done
183
    with End_of_file -> ()
184

    
185
let choiceGraph () =
186
  choiceSat ();
187
  print_endline "digraph reasonerstate {";
188
  CM.graphIterCores (fun core -> print_endline (CM.coreToDot core));
189
  CM.graphIterStates (fun state -> print_endline (CM.stateToDot state));
190
  print_endline "}"
191

    
192
let choiceVerify () =
193
    try
194
      while true do
195
        let input = read_line () in
196
        if not (GenAndComp.isEmptyString input) then
197
          let f = CoAlgFormula.importFormula input in
198
          let str = CoAlgFormula.exportFormula f in
199
          incr counter;
200
          print_string ("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
201
          flush stdout;
202
          CoAlgFormula.verifyFormula f;
203
        else ()
204
      done
205
    with End_of_file -> ()
206

    
207
let rec parseFlags arr offs : unit =
208
    let offs = ref (offs) in
209
    let getParam () =
210
        if ((!offs + 1) >= Array.length arr) then
211
            raise (CoAlgFormula.CoAlgException ("Parameter missing for flag »" ^ (arr.(!offs)) ^ "«"))
212
        else
213
            offs := !offs + 1;
214
            arr.(!offs)
215
    in
216
    if (!offs >= Array.length arr) then ()
217
    else (ignore (match arr.(!offs) with
218
         | "--verbose" -> verbose := true
219
         | "--agents" ->
220
            let strAglist = getParam () in
221
            let aglist = List.map int_of_string (Str.split (Str.regexp ",") strAglist) in
222
            CoolUtils.cl_set_agents (Array.of_list aglist)
223
         | _ ->
224
            raise (CoAlgFormula.CoAlgException ("Unknown flag »" ^ (arr.(!offs)) ^ "«"))
225
         ) ; parseFlags arr (!offs + 1)
226
     )
227

    
228
let _ =
229
  if Array.length Sys.argv < 3 then printUsage()
230
  else
231
    let choice = Sys.argv.(1) in
232
    parseFlags Sys.argv 3;
233
    match choice with
234
    | "sat" -> choiceSat ()
235
    | "prov" -> choiceProvable ()
236
    | "print" -> choicePrint ()
237
    | "nnf" -> choiceNNF ()
238
    | "verify" -> choiceVerify ()
239
    | "graph" -> choiceGraph ()
240
	| "nom2fix" -> choiceNom2fix()
241
    | _ -> printUsage ()