add 'frenetic decide' command that reads in file and decides equivale…

…nce.

examples/decision-procedure/malvin.kat

@@ -0,0 +1 @@
+((ag=0;pt=1;Saa=1;Sab=0;Sac=0;Naa=1;Nab=1;Nac=0;Sba=0;Sbb=1;Sbc=0;Nba=0;Nbb=1;Nbc=1;Sca=0;Scb=0;Scc=1;Nca=0;Ncb=0;Ncc=1);(((ag:=0;pt:=1)+(ag:=1;pt:=4)+(ag:=2;pt:=7));(((ag=0;pt=1;Sab=0;Nab=1;((((Saa=1;Sba:=1)+Saa=0);((Sba=1;Saa:=1)+Sba=0);((Naa=1;Nba:=1)+Naa=0);((Nba=1;Naa:=1)+Nba=0));(((Sab=1;Sbb:=1)+Sab=0);((Sbb=1;Sab:=1)+Sbb=0);((Nab=1;Nbb:=1)+Nab=0);((Nbb=1;Nab:=1)+Nbb=0));(((Sac=1;Sbc:=1)+Sac=0);((Sbc=1;Sac:=1)+Sbc=0);((Nac=1;Nbc:=1)+Nac=0);((Nbc=1;Nac:=1)+Nbc=0))))+(ag=0;pt=1;Sac=0;Nac=1;((((Saa=1;Sca:=1)+Saa=0);((Sca=1;Saa:=1)+Sca=0);((Naa=1;Nca:=1)+Naa=0);((Nca=1;Naa:=1)+Nca=0));(((Sab=1;Scb:=1)+Sab=0);((Scb=1;Sab:=1)+Scb=0);((Nab=1;Ncb:=1)+Nab=0);((Ncb=1;Nab:=1)+Ncb=0));(((Sac=1;Scc:=1)+Sac=0);((Scc=1;Sac:=1)+Scc=0);((Nac=1;Ncc:=1)+Nac=0);((Ncc=1;Nac:=1)+Ncc=0)))))+(((ag=1;pt=4;Sba=0;Nba=1;((((Sba=1;Saa:=1)+Sba=0);((Saa=1;Sba:=1)+Saa=0);((Nba=1;Naa:=1)+Nba=0);((Naa=1;Nba:=1)+Naa=0));(((Sbb=1;Sab:=1)+Sbb=0);((Sab=1;Sbb:=1)+Sab=0);((Nbb=1;Nab:=1)+Nbb=0);((Nab=1;Nbb:=1)+Nab=0));(((Sbc=1;Sac:=1)+Sbc=0);((Sac=1;Sbc:=1)+Sac=0);((Nbc=1;Nac:=1)+Nbc=0);((Nac=1;Nbc:=1)+Nac=0))))+(ag=1;pt=4;Sbc=0;Nbc=1;((((Sba=1;Sca:=1)+Sba=0);((Sca=1;Sba:=1)+Sca=0);((Nba=1;Nca:=1)+Nba=0);((Nca=1;Nba:=1)+Nca=0));(((Sbb=1;Scb:=1)+Sbb=0);((Scb=1;Sbb:=1)+Scb=0);((Nbb=1;Ncb:=1)+Nbb=0);((Ncb=1;Nbb:=1)+Ncb=0));(((Sbc=1;Scc:=1)+Sbc=0);((Scc=1;Sbc:=1)+Scc=0);((Nbc=1;Ncc:=1)+Nbc=0);((Ncc=1;Nbc:=1)+Ncc=0)))))+((ag=2;pt=7;Sca=0;Nca=1;((((Sca=1;Saa:=1)+Sca=0);((Saa=1;Sca:=1)+Saa=0);((Nca=1;Naa:=1)+Nca=0);((Naa=1;Nca:=1)+Naa=0));(((Scb=1;Sab:=1)+Scb=0);((Sab=1;Scb:=1)+Sab=0);((Ncb=1;Nab:=1)+Ncb=0);((Nab=1;Ncb:=1)+Nab=0));(((Scc=1;Sac:=1)+Scc=0);((Sac=1;Scc:=1)+Sac=0);((Ncc=1;Nac:=1)+Ncc=0);((Nac=1;Ncc:=1)+Nac=0))))+(ag=2;pt=7;Scb=0;Ncb=1;((((Sca=1;Sba:=1)+Sca=0);((Sba=1;Sca:=1)+Sba=0);((Nca=1;Nba:=1)+Nca=0);((Nba=1;Nca:=1)+Nba=0));(((Scb=1;Sbb:=1)+Scb=0);((Sbb=1;Scb:=1)+Sbb=0);((Ncb=1;Nbb:=1)+Ncb=0);((Nbb=1;Ncb:=1)+Nbb=0));(((Scc=1;Sbc:=1)+Scc=0);((Sbc=1;Scc:=1)+Sbc=0);((Ncc=1;Nbc:=1)+Ncc=0);((Nbc=1;Ncc:=1)+Nbc=0))))))))*;((Nab=0+Sab=1);(Nac=0+Sac=1);(Nba=0+Sba=1);(Nbc=0+Sbc=1);(Nca=0+Sca=1);(Ncb=0+Scb=1))) == ((ag=0;pt=1;Saa=1;Sab=0;Sac=0;Naa=1;Nab=1;Nac=0;Sba=0;Sbb=1;Sbc=0;Nba=0;Nbb=1;Nbc=1;Sca=0;Scb=0;Scc=1;Nca=0;Ncb=0;Ncc=1);(((ag:=0;pt:=1)+(ag:=1;pt:=4)+(ag:=2;pt:=7));(((ag=0;pt=1;Sab=0;Nab=1;((((Saa=1;Sba:=1)+Saa=0);((Sba=1;Saa:=1)+Sba=0);((Naa=1;Nba:=1)+Naa=0);((Nba=1;Naa:=1)+Nba=0));(((Sab=1;Sbb:=1)+Sab=0);((Sbb=1;Sab:=1)+Sbb=0);((Nab=1;Nbb:=1)+Nab=0);((Nbb=1;Nab:=1)+Nbb=0));(((Sac=1;Sbc:=1)+Sac=0);((Sbc=1;Sac:=1)+Sbc=0);((Nac=1;Nbc:=1)+Nac=0);((Nbc=1;Nac:=1)+Nbc=0))))+(ag=0;pt=1;Sac=0;Nac=1;((((Saa=1;Sca:=1)+Saa=0);((Sca=1;Saa:=1)+Sca=0);((Naa=1;Nca:=1)+Naa=0);((Nca=1;Naa:=1)+Nca=0));(((Sab=1;Scb:=1)+Sab=0);((Scb=1;Sab:=1)+Scb=0);((Nab=1;Ncb:=1)+Nab=0);((Ncb=1;Nab:=1)+Ncb=0));(((Sac=1;Scc:=1)+Sac=0);((Scc=1;Sac:=1)+Scc=0);((Nac=1;Ncc:=1)+Nac=0);((Ncc=1;Nac:=1)+Ncc=0)))))+(((ag=1;pt=4;Sba=0;Nba=1;((((Sba=1;Saa:=1)+Sba=0);((Saa=1;Sba:=1)+Saa=0);((Nba=1;Naa:=1)+Nba=0);((Naa=1;Nba:=1)+Naa=0));(((Sbb=1;Sab:=1)+Sbb=0);((Sab=1;Sbb:=1)+Sab=0);((Nbb=1;Nab:=1)+Nbb=0);((Nab=1;Nbb:=1)+Nab=0));(((Sbc=1;Sac:=1)+Sbc=0);((Sac=1;Sbc:=1)+Sac=0);((Nbc=1;Nac:=1)+Nbc=0);((Nac=1;Nbc:=1)+Nac=0))))+(ag=1;pt=4;Sbc=0;Nbc=1;((((Sba=1;Sca:=1)+Sba=0);((Sca=1;Sba:=1)+Sca=0);((Nba=1;Nca:=1)+Nba=0);((Nca=1;Nba:=1)+Nca=0));(((Sbb=1;Scb:=1)+Sbb=0);((Scb=1;Sbb:=1)+Scb=0);((Nbb=1;Ncb:=1)+Nbb=0);((Ncb=1;Nbb:=1)+Ncb=0));(((Sbc=1;Scc:=1)+Sbc=0);((Scc=1;Sbc:=1)+Scc=0);((Nbc=1;Ncc:=1)+Nbc=0);((Ncc=1;Nbc:=1)+Ncc=0)))))+((ag=2;pt=7;Sca=0;Nca=1;((((Sca=1;Saa:=1)+Sca=0);((Saa=1;Sca:=1)+Saa=0);((Nca=1;Naa:=1)+Nca=0);((Naa=1;Nca:=1)+Naa=0));(((Scb=1;Sab:=1)+Scb=0);((Sab=1;Scb:=1)+Sab=0);((Ncb=1;Nab:=1)+Ncb=0);((Nab=1;Ncb:=1)+Nab=0));(((Scc=1;Sac:=1)+Scc=0);((Sac=1;Scc:=1)+Sac=0);((Ncc=1;Nac:=1)+Ncc=0);((Nac=1;Ncc:=1)+Nac=0))))+(ag=2;pt=7;Scb=0;Ncb=1;((((Sca=1;Sba:=1)+Sca=0);((Sba=1;Sca:=1)+Sba=0);((Nca=1;Nba:=1)+Nca=0);((Nba=1;Nca:=1)+Nba=0));(((Scb=1;Sbb:=1)+Scb=0);((Sbb=1;Scb:=1)+Sbb=0);((Ncb=1;Nbb:=1)+Ncb=0);((Nbb=1;Ncb:=1)+Nbb=0));(((Scc=1;Sbc:=1)+Scc=0);((Sbc=1;Scc:=1)+Sbc=0);((Ncc=1;Nbc:=1)+Ncc=0);((Nbc=1;Ncc:=1)+Nbc=0))))))))*;((Saa=1;Sab=1;Sac=1);(Sba=1;Sbb=1;Sbc=1);(Sca=1;Scb=1;Scc=1)))

frenetic/frenetic.ml

@@ -145,6 +145,33 @@ let openflow13_fault_tolerant_controller : Command.t =
       run (Frenetic_OpenFlow0x04_Plugin.fault_tolerant_main
         openflow_port policy_file topology_file))
 
+
+
+let decide : Command.t =
+  Command.basic
+    ~summary:"Invokes decision procedure with provided file."
+    Command.Spec.(
+      empty
+      +> anon ("file" %: file)
+    )
+    (fun file () ->
+      In_channel.with_file file ~binary:false ~f:(fun in_ch ->
+        (* code copied from Frenetic_Shell and adapted to work with stream *)
+        let open Frenetic_Shell in
+        try
+          let lexbuf = Lexing.from_channel in_ch in
+          let formula = parse_exn DecideParser.formula_main lexbuf "" in
+          (* TODO(mwhittaker). This doesn't handle formulas with <= in them
+           * correctly. See test_lib/Test_Decide.ml for the correct behavior. *)
+          let lhs, rhs = DecideAst.Formula.terms formula in
+          ignore (DecideUtil.set_univ DecideAst.([Term.values lhs; Term.values rhs]));
+          printf "%b\n%!" (Frenetic_Decide_Bisimulation.check_equivalent lhs rhs)
+        with
+        | ParseError (filename, line, char, token) ->
+            printf "Parse error %s:%d%d: %s\n%!" filename line char token
+      )
+    )
+
 let main : Command.t =
   Command.group
     ~summary:"Invokes the specified Frenetic module."
@@ -153,7 +180,8 @@ let main : Command.t =
     ; ("http-controller", http_controller)
     ; ("openflow13", openflow13_controller)
     ; ("fault-tolerant", openflow13_fault_tolerant_controller)
-    ; ("dump", Dump.main)]
+    ; ("dump", Dump.main)
+    ; ("decide", decide)]
 
 let () =
   Command.run ~version: "5.0" ~build_info: "RWO" main