Kim Nguyễn [Sun, 24 Nov 2013 21:18:57 +0000 (22:18 +0100)]
Add a tiny XML file to help debug automata behaviour.
Kim Nguyễn [Wed, 20 Nov 2013 21:50:56 +0000 (22:50 +0100)]
Put the move type of automata in a Move module and add auxiliary function to create and maintain tables indexed by moves. Use it to return the states of a forumla by move.
Kim Nguyễn [Wed, 20 Nov 2013 21:46:24 +0000 (22:46 +0100)]
Add a utility function Boolean.iter that iterates a function over a formula.
Kim Nguyễn [Sat, 16 Nov 2013 22:06:32 +0000 (23:06 +0100)]
Remove useless cycles in the generated automaton. A state now only has at most one trivial cycle with itself.
Kim Nguyễn [Fri, 22 Nov 2013 14:32:07 +0000 (15:32 +0100)]
Silence an unused variable warning.
Kim Nguyễn [Fri, 8 Nov 2013 21:21:02 +0000 (22:21 +0100)]
Print detailed statisticts of the run.
Kim Nguyễn [Fri, 8 Nov 2013 20:43:29 +0000 (21:43 +0100)]
Add a script to output the number of states/running time/number of traversal for increasing query sizes.
Kim Nguyễn [Tue, 1 Oct 2013 20:12:27 +0000 (22:12 +0200)]
Fix a bug in the compilation of * tests.
Kim Nguyễn [Sun, 18 Aug 2013 16:49:58 +0000 (18:49 +0200)]
Add the .mly and .mll files as dependencies of the generated .ml
Kim Nguyễn [Sun, 18 Aug 2013 16:32:18 +0000 (18:32 +0200)]
Refactor HTML tracing utility. Color the nodes that are in the same
sat configuration in the same color.
Kim Nguyễn [Sun, 18 Aug 2013 10:19:08 +0000 (12:19 +0200)]
Increase the size of the border of selected nodes in the html trace.
Kim Nguyễn [Sun, 18 Aug 2013 10:18:26 +0000 (12:18 +0200)]
Also print the number of states when printing automata.
Kim Nguyễn [Fri, 16 Aug 2013 17:42:17 +0000 (19:42 +0200)]
Do not update the run if the todo set is empty for the current node.
Kim Nguyễn [Thu, 15 Aug 2013 15:11:02 +0000 (17:11 +0200)]
Rewrite the HTML debugging output to generate an svg file directly instead going
through graphviz.
Kim Nguyễn [Wed, 14 Aug 2013 08:59:27 +0000 (10:59 +0200)]
Add fold_left/right functions to the set interface (iterate in
increasing/decreasing order of keys).
Kim Nguyễn [Wed, 7 Aug 2013 17:21:15 +0000 (19:21 +0200)]
Implement set-theoretic operation on 2WSATA (union, intersection,
negation, difference).
Kim Nguyễn [Wed, 7 Aug 2013 10:36:39 +0000 (12:36 +0200)]
Implement reverse mapping from preorder to nodes.
Kim Nguyễn [Wed, 7 Aug 2013 10:34:51 +0000 (12:34 +0200)]
Improve performance of parallel run by replacing standard hashtable with
Cache.N1 array.
Kim Nguyễn [Sat, 27 Jul 2013 14:32:26 +0000 (16:32 +0200)]
Lowlevel optimizations in the Ptset module, replace some function
calls by a field access, use bit twidling hack to compute the
largest power of two inferior to a given value (was previously done
with log(WORDSIZE * 8) branching + table lookup).
Kim Nguyễn [Fri, 26 Jul 2013 15:16:13 +0000 (17:16 +0200)]
Do not stupidely recompute a constant set of states for each node
in the tree, compute it once and for all before the run and store it
at each node as we traverse them.
Kim Nguyễn [Fri, 26 Jul 2013 14:38:26 +0000 (16:38 +0200)]
Improve performances by moving the caching outside of the saturation
of the set of states of the current node (instead of caching and
looking-up at each step)
Kim Nguyễn [Fri, 26 Jul 2013 14:01:29 +0000 (16:01 +0200)]
Drastically improve performances by simplifying the book-keeping
of pending transitions during a topdown run.
Before:
- we were keeping for each node
(1) sat: the set of states satisfied at that node
(2) unsat: the set of states unsatisfied at that node
(3) todo: the hashconsed list of pending transitions (of the
form q, {a,b,c} -> f
where f has been simplified w.r.t to sat and unsat (that is
atoms containing states in either have been simplified to True
or False) and q is neither in sat nor unsat.
- during each run, for each node, we were scanning todo and rebuilding
it removing satisfied or unsatisfied transitions. This lead to excessive
hashconsing, and a lot of time spent in the hashconsing module (in turn
spending a lot of time in the GC)
After:
- we keep for each node:
(1) sat: the set of states satisfied at that node
(2) todo: the set of undetermined *states*
- we perform the book-keeping as before but do not materialize the
simplified transitions. Also unsat is made inplicit (a state is
unsat if it is neither in sat nor todo).
Kim Nguyễn [Thu, 25 Jul 2013 13:24:58 +0000 (15:24 +0200)]
Revert "Tentative optimization"
This reverts commit
e9b4969905125718589b18ff6286e05688f7a929.
Avoiding the computation of a simplified formula does not help.
Kim Nguyễn [Thu, 25 Jul 2013 13:22:00 +0000 (15:22 +0200)]
Add gmon.out to .gitignore
Kim Nguyễn [Thu, 25 Jul 2013 13:21:36 +0000 (15:21 +0200)]
Tentative optimization
Kim Nguyễn [Thu, 25 Jul 2013 09:26:56 +0000 (11:26 +0200)]
Factor Remakefie and add more tests for parallel query composition.
Kim Nguyễn [Thu, 25 Jul 2013 07:09:58 +0000 (09:09 +0200)]
Add Makefile to .gitignore
Kim Nguyễn [Wed, 24 Jul 2013 22:12:14 +0000 (00:12 +0200)]
Add a Makefile to drive the build process.
Kim Nguyễn [Wed, 24 Jul 2013 21:59:01 +0000 (23:59 +0200)]
Fix invalid variable substitution in buildscript.
Kim Nguyễn [Wed, 24 Jul 2013 21:52:16 +0000 (23:52 +0200)]
Update the output of the reference implementation to the new format.
Kim Nguyễn [Wed, 24 Jul 2013 21:50:43 +0000 (23:50 +0200)]
Remove un-needed scripts
Kim Nguyễn [Wed, 24 Jul 2013 21:49:44 +0000 (23:49 +0200)]
Factorise common bits of Remakefile in tools/ocamldriver.sh
Kim Nguyễn [Wed, 24 Jul 2013 20:52:03 +0000 (22:52 +0200)]
Refactor the build process. Piggyback on remake's dependency tracking
to perform a topological sort of the object files, used during linking.
This is done by generating a .dep file for each object file keeping in
a .dep the transitive closure of its dependencies.
Also, packed modules must now be described by:
- a directory
- a file with the .pack extension, with the same basename as the directory,
listing the module names (relative to the directory containing the .ml files)
Kim Nguyễn [Wed, 24 Jul 2013 15:21:56 +0000 (17:21 +0200)]
Add more tests (broken, needs a refactoring of the build script)
Kim Nguyễn [Wed, 24 Jul 2013 09:49:53 +0000 (11:49 +0200)]
Add tests for parallel query evaluation.
Kim Nguyễn [Tue, 23 Jul 2013 17:06:50 +0000 (19:06 +0200)]
Implement the multiple-starters feature:
- implement automata merging and concatenation
- change the command line parsing to allow multiple queries
- update the output format to denote which query a result set belongs to
- implement full evaluation of automata (associate each selecting state
with its result set)
Given queries Q1 ... QN on the command line, we can now:
- compute Q1, then Q2, ... , then QN on the same document, sequentially
- build one automaton that computes Q1, ..., QN in parallel
- compute QN(... Q2(Q1(root))) sequentially (materializing intermediate
results)
- build one automaton that computes QN(...(Q2(Q1(root)))) in one run.
Kim Nguyễn [Tue, 23 Jul 2013 07:38:39 +0000 (09:38 +0200)]
Change command line options:
* -d, --doc set the input document (default to stdin)
* -o, --out set the output file (default to stdout)
Kim Nguyễn [Tue, 23 Jul 2013 06:50:13 +0000 (08:50 +0200)]
Implement copy and composition of automata.
Kim Nguyễn [Fri, 19 Jul 2013 15:02:10 +0000 (17:02 +0200)]
Preliminary work for multiple starters evaluation.
Kim Nguyễn [Fri, 19 Jul 2013 13:33:37 +0000 (15:33 +0200)]
Refactor the Ata module:
- add a builder class to ensure we only manipulate well-formed automata
- move all the caching infrastructure to the computation of the run
- rename the Eval module to Run
Kim Nguyễn [Wed, 17 Jul 2013 15:59:01 +0000 (17:59 +0200)]
Sanitize the representation of formula
- rename the toplevel Formula module to Boolean
- rename Ata.SFormula to Formula
- move the flag saying whether an atom is positive or negative
to Boolean
- distinguish predicates that are moves from generic predicates.
Kim Nguyễn [Wed, 17 Jul 2013 16:00:58 +0000 (18:00 +0200)]
Add a bullet symbol.
Kim Nguyễn [Wed, 17 Jul 2013 16:00:43 +0000 (18:00 +0200)]
Add an int_of_bool cast function.
Kim Nguyễn [Wed, 17 Jul 2013 16:00:22 +0000 (18:00 +0200)]
Add an interface for the evaluation module.
Kim Nguyễn [Wed, 17 Jul 2013 12:32:56 +0000 (14:32 +0200)]
Make remake change to the directory where ./remake (and the Remakefile) are.
Kim Nguyễn [Mon, 15 Jul 2013 15:46:15 +0000 (17:46 +0200)]
Remove the timestamp header in source files. This information is
better kept in git.
Kim Nguyễn [Mon, 15 Jul 2013 15:37:39 +0000 (17:37 +0200)]
Fix a bug where the content of variables are appended instead of being
overwritten. Thus, when several sub-process send variable A=foo to the
server, the content of A becomes foofoofoofoo instead of just foo.
Kim Nguyễn [Mon, 15 Jul 2013 15:37:05 +0000 (17:37 +0200)]
Fix a typo which causes mis-detection of the ocaml-expat bindings.
Kim Nguyễn [Fri, 7 Jun 2013 15:44:41 +0000 (17:44 +0200)]
Migrate to new remake.
Kim Nguyễn [Fri, 26 Apr 2013 14:55:55 +0000 (16:55 +0200)]
Remove the 'round' counter from the hashconsed configurations.
Kim Nguyễn [Thu, 25 Apr 2013 13:35:52 +0000 (15:35 +0200)]
Add a clean logger infrastructure.
Kim Nguyễn [Wed, 24 Apr 2013 16:42:24 +0000 (18:42 +0200)]
Add a bitmap to keep track of whether a subtree needs to be
recomputed or not.
A subtree needs to be recomputed when:
(1) it's todo transition list is not empty or
(2) one of its subtrees needs to be recomputed.
Introduce a bitvector module to efficiently represent arrays of
booleans.
Kim Nguyễn [Wed, 24 Apr 2013 16:43:23 +0000 (18:43 +0200)]
Update test results.
Kim Nguyễn [Tue, 23 Apr 2013 14:58:08 +0000 (16:58 +0200)]
Make the html trace tools use colors to represent the round at
which an node was satisfied.
Kim Nguyễn [Tue, 23 Apr 2013 14:57:59 +0000 (16:57 +0200)]
Add a new test suite.
Kim Nguyễn [Tue, 23 Apr 2013 13:03:33 +0000 (15:03 +0200)]
Cosmetic changes.
Kim Nguyễn [Tue, 23 Apr 2013 09:37:10 +0000 (11:37 +0200)]
Add generated files to the .gitignore.
Kim Nguyễn [Tue, 23 Apr 2013 09:36:10 +0000 (11:36 +0200)]
Last tweaking of the Remakefile for automated testing.
Kim Nguyễn [Mon, 22 Apr 2013 16:49:11 +0000 (18:49 +0200)]
Tune the Remakefile to re-run tests when the binary changes.
Kim Nguyễn [Mon, 22 Apr 2013 16:20:49 +0000 (18:20 +0200)]
Use the Remakefile to perform non-regression tests.
Kim Nguyễn [Mon, 22 Apr 2013 15:27:59 +0000 (17:27 +0200)]
Implement command line options, clean-up screen output.
Kim Nguyễn [Mon, 22 Apr 2013 13:34:39 +0000 (15:34 +0200)]
Merge branch 'feature/precise-sat'
Kim Nguyễn [Mon, 22 Apr 2013 13:33:58 +0000 (15:33 +0200)]
Hashcons transition evaluation based on node configuration.
Kim Nguyễn [Mon, 22 Apr 2013 12:48:11 +0000 (14:48 +0200)]
Store a summary of the node (kind, topology) in the Ata.Config.t type.
Kim Nguyễn [Thu, 18 Apr 2013 23:25:02 +0000 (01:25 +0200)]
add OCaml object files to .gitignore
Kim Nguyễn [Thu, 18 Apr 2013 23:23:40 +0000 (01:23 +0200)]
Hash-conses each node configuration.
Kim Nguyễn [Thu, 18 Apr 2013 16:14:29 +0000 (18:14 +0200)]
Fix the Remakefile and testing script.
Kim Nguyễn [Thu, 18 Apr 2013 16:14:44 +0000 (18:14 +0200)]
Maintain the set of unsatisfiable states.
Kim Nguyễn [Thu, 18 Apr 2013 16:14:29 +0000 (18:14 +0200)]
Fix the Remakefile and testing script.
Kim Nguyễn [Thu, 18 Apr 2013 09:28:58 +0000 (11:28 +0200)]
Add an INSTALL file.
Kim Nguyễn [Thu, 18 Apr 2013 09:27:51 +0000 (11:27 +0200)]
Re-organize the Remakefile.
Fixes a few typos and make remake.cpp callable from subdirectories.
Kim Nguyễn [Wed, 17 Apr 2013 06:48:53 +0000 (08:48 +0200)]
Make the main target more generic, to allow compilation of
tools/*.native too, instead of only src/*.native.
Kim Nguyễn [Wed, 17 Apr 2013 06:18:44 +0000 (08:18 +0200)]
Add a distclean target that removes every file generated by the
configure/remake scripts.
Kim Nguyễn [Wed, 17 Apr 2013 06:12:53 +0000 (08:12 +0200)]
Modified building instructions.
Kim Nguyễn [Wed, 17 Apr 2013 06:09:31 +0000 (08:09 +0200)]
Remove OCamlbuild related files. Youpi.
Kim Nguyễn [Wed, 17 Apr 2013 06:08:10 +0000 (08:08 +0200)]
Add the remake and configure infrastructure.
Kim Nguyễn [Wed, 17 Apr 2013 06:06:11 +0000 (08:06 +0200)]
Fix remaining compilation bug caused by the refactoring of modules.
(Bug was previously unnoticed because it only touches code that handle
tracing of automaton run)
Kim Nguyễn [Wed, 17 Apr 2013 06:05:00 +0000 (08:05 +0200)]
Add configure and remake generated files to .gitignore
Kim Nguyễn [Thu, 4 Apr 2013 19:16:44 +0000 (21:16 +0200)]
Merge branch 'master' of ssh://git.nguyen.vg/tatoo
* 'master' of ssh://git.nguyen.vg/tatoo:
Flatten the sources, only leave the XPath module packed.
Fix the build script.
Kim Nguyễn [Thu, 4 Apr 2013 16:48:43 +0000 (18:48 +0200)]
Flatten the sources, only leave the XPath module packed.
Kim Nguyễn [Thu, 4 Apr 2013 14:17:32 +0000 (16:17 +0200)]
Fix the build script.
Kim Nguyễn [Sat, 23 Mar 2013 18:44:48 +0000 (19:44 +0100)]
Add AUTHORS file
Kim Nguyễn [Sat, 23 Mar 2013 14:30:28 +0000 (15:30 +0100)]
Printout statistics about cache occupation.
Kim Nguyễn [Sat, 23 Mar 2013 14:30:06 +0000 (15:30 +0100)]
Silences the newly introduced K warning (unused functions)
Kim Nguyễn [Sat, 16 Mar 2013 10:32:08 +0000 (11:32 +0100)]
- Reorder the keys used to cache transitions
- Use a new stop condition (gives optimal traversal for filter
less queries)
- Reorder a variant type so that the hash of some variant becomes
smaller
Kim Nguyễn [Sat, 16 Mar 2013 05:57:30 +0000 (06:57 +0100)]
Display caching and iteration statistics at the end of evaluation.
Kim Nguyễn [Fri, 15 Mar 2013 22:25:18 +0000 (23:25 +0100)]
Simplify transition instead of evaluating them to true/false.
Kim Nguyễn [Fri, 15 Mar 2013 22:02:15 +0000 (23:02 +0100)]
Add the JAXP reference files to the repository.
Kim Nguyễn [Fri, 15 Mar 2013 21:25:55 +0000 (22:25 +0100)]
Rework the test script.
Kim Nguyễn [Fri, 15 Mar 2013 22:41:16 +0000 (23:41 +0100)]
Add debugging information to the automaton.
Kim Nguyễn [Fri, 15 Mar 2013 17:47:34 +0000 (18:47 +0100)]
Modify the testing scripts.
Kim Nguyễn [Fri, 15 Mar 2013 16:31:59 +0000 (17:31 +0100)]
Code refactoring:
- move the caching tables inside the automaton object
- add an interface for the ata module
- make the automaton record type private
Kim Nguyễn [Fri, 15 Mar 2013 14:23:11 +0000 (15:23 +0100)]
Make the output graph nodes rectangular.
Kim Nguyễn [Thu, 14 Mar 2013 20:29:39 +0000 (21:29 +0100)]
Add a 'trace' mode (must be enabled at build time) that saves the
tree and all information to a browsable svg.
Kim Nguyễn [Thu, 14 Mar 2013 12:52:31 +0000 (13:52 +0100)]
Write the caching module in a more systematic way.
Kim Nguyễn [Thu, 14 Mar 2013 10:26:51 +0000 (11:26 +0100)]
Reuse the same cache between different iterations.
Kim Nguyễn [Thu, 14 Mar 2013 07:20:05 +0000 (08:20 +0100)]
Rework the testing script.
Rename the main program.
Kim Nguyễn [Wed, 13 Mar 2013 20:53:44 +0000 (21:53 +0100)]
Make the program report query execution time and query serialization time.
Kim Nguyễn [Wed, 13 Mar 2013 18:06:10 +0000 (19:06 +0100)]
Staturate the set of state of the current node to avoid some traversal.
Kim Nguyễn [Wed, 13 Mar 2013 17:54:21 +0000 (18:54 +0100)]
Replace the Hashtbl.t used for mapping nodes to state-sets by an
array indexed by pre-order.