What's in the Directories?

Here are the main directories of Toss source code, in order of dependency, i.e. the first one listed does not depend on anything else, and the last one contains the main executable and uses all previous ones.

• Formula contains the type definition for formulas and functions which operate on formulas only — substitutions for variables, normal forms, simplifications, parsing and printing. We also keep the module Aux, with many useful auxiliary functions, in this directory.
• Term contains the type definition for typed terms and functions for term rewriting, type reconstruction and type-aware parsing. It also contains a basic term rewriting language which is then used for example for defining structures.
• Solver directory contains type definitions for structures, variable assignments to structure elements, and the solver module for calculating the assignments which satisfy a formula on a structure.
• Arena is the directory in which we define structure rewriting games — discrete and continuous rewriting rules first, and finally the whole games in the Arena module. Discrete rule application is handled in the DiscreteRule module by translating rules to formulas and using the solver. Continuous dynamics is split into the Term module and ContinuousRule. The parser for complete Toss games, i.e. the .toss files, is defined in ArenaParser.mly.
• Play contains the modules related to making Toss play any defined game automatically — we generate heuristics in the Heuristic module and use GameTree to implement a search to finally Play.
• GGP is a directory devoted to translating games in the GDL language (Game Description Language) to the Toss format. We implement GDL parsing, basic operations, stepwise translation and finally some simplification of the resulting games. There are also tests in the GGP/examples sub-directory.
• Learn contains our learning algorithms. This includes the Hintikka-formulas based algorithm for differentiating structures by formulas of various logics, which is then used to learn games from example plays, as well as the SAT-solver based algorithms. The sat-based ones are used to automatically learn reductions between complexity classes, learn LFP formulas given a specification, and can also be used to learn game rules. We also keep there a program to recognize plays from videos, which allows to go from video demonstrations to game playing.
• Vision has some basic vision algorithms that we started in an ongoing effort to bring game learning to our web interface.
• Server contains the main executable of Toss (in the file Server.ml) and the main request handler in the ReqHandler module, with other files as needed (e.g. database connection handler in DB). We also keep the lists of all unit tests there, in Server/Tests.ml.

The command make TossTestFull runs all unit tests for all modules from all directories. As this takes some time, we often execute only a subset of fast-running tests by make TossTest.

Adding Your Module

Code in Toss is organized in a way analogous to the one presented in our Mini OCaml Tutorial. Thus, to start coding new functions with Toss, you should add 3 Files: an ml file with your functions, an mli file with the interface (and for documentation) and an ...Test.ml file with your calls and unit tests. As described above, the directories are organized hierarchically, so if you intend to only operate on formulas, you should add your module to the Formula directory. If you want to be able to use all functions of Toss (or just not worry about the dependencies for now), add your module to the Server directory, which includes all other directories in its dependency list.
As a starting example, let's add a module that parses a formula and a structure from strings and returns a print-out of the satisfying assignments. Here is the interface (mli file) assuming we name the module MyModule and put it is Server directory.

(** This is just a sample module. *)

(** Parse a formula and a structure and return the satisfying assignments. *)
val show_satisfying : formula: string -> structure: string -> string
    

This function can be implemented as follows.

let formula_of_string s = 
  FormulaParser.parse_formula Lexer.lex (Lexing.from_string s)

let structure_of_string s = 
  StructureParser.parse_structure Lexer.lex (Lexing.from_string s)

let show_satisfying ~formula ~structure =
  let (f, struc) = (formula_of_string formula, structure_of_string structure) in
  AssignmentSet.str (Solver.M.evaluate struc f)
    

To test this function, we need to add a file with unit tests, e.g. this one.

open OUnit

let tests = "MyModule" >::: [
  "show_satisfying" >::
    (fun () ->
      assert_equal ~printer:(fun x -> x) 
	"???"
	(MyModule.show_satisfying 
	   ~structure:"[ | R { (a, b); (a, c) } | ]"
	   ~formula:"ex x R (x, y)");
    );
]
    

Note that, since we are not sure about the result of the call yet, we left ??? as the expected value of this test — it should fail and tell us the value returned by the program. But how do we run the test? As described in the Mini OCaml Tutorial, we do not run the tests separately but execute them all from the main Toss file. To add MyModuleTest.tests to the list of executed tests, edit the file Server/Tests.ml and add one line after the let server_tests = "Server" line. This part should now look as follows.

...
let server_tests = "Server", [
  "MyModuleTest",     [MyModuleTest.tests];
...
    

We can now compile and run the tests by running make MyModuleTest from the Server directory, or make Server/MyModuleTest from the main Toss directory.

~/Toss/Server$ make MyModuleTest
~/Toss$ make Server/MyModuleTest
    

Note that, in fact, it is the main TossServer file that is executed, and an option specifies which test should be run. The result is, as expected, a failure.

Failure: Toss:0:Server:0:MyModule:0:show_satisfying

OUnit: expected: ?? but got: { y->2, y->3 }      
    

And indeed — the right assignment for the given formula on the structure we entered is y equal to 2 or 3, so we can correct the test now.

open OUnit

let tests = "MyModule" >::: [
  "show_satisfying" >::
    (fun () ->
      assert_equal ~printer:(fun x -> x) 
	"{ y->2, y->3 }"
	(MyModule.show_satisfying 
	   ~structure:"[ | R { (a, b); (a, c) } | ]"
	   ~formula:"ex x R (x, y)");
    );
]
    

and check that the answer is correct.

~/Toss$ make Server/MyModuleTest
ocamlbuild -log build.log -j 8 -menhir ../menhir_conf 
  -pp "camlp4o ../caml_extensions/pa_let_try.cmo" -libs str,nums,unix,oUnit,sqlite3
  -cflags -I,+oUnit,-I,+sqlite3,-I,+site-lib/oUnit,-I,+site-lib/sqlite3,-g 
  -lflags -I,+oUnit,-I,+sqlite3,-I,+site-lib/oUnit,-I,+site-lib/sqlite3
  -Is Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver,Arena,Play,GGP
  Server/Server.native
Finished, 336 targets (332 cached) in 00:00:02.
cp _build/Server/Server.native TossServer
OCAMLRUNPARAM=b; export OCAMLRUNPARAM; \
	  ./TossServer -fulltest Server/MyModuleTest
.
Ran: 1 tests in: 0.00 seconds.
    

Example Toss Calls

Already in the section above, we have shown how to call the Formula Parser to parse formulas and the Structure Parser to parse a structure. We called the Solver.M module to evaluate the formula (we call it Solver.M and not just Solver to make it easier to substitute other solvers and experiment with different solving methods). Finally, to print out the resulting set of assignments, we used the basic str function from the Assignment Set module.