Kim Nguyễn [Wed, 12 Apr 2017 09:30:11 +0000 (11:30 +0200)]
Add a compact tree model.
Kim Nguyễn [Wed, 12 Apr 2017 06:51:31 +0000 (08:51 +0200)]
Add a generic deque module.
Kim Nguyễn [Mon, 3 Apr 2017 09:17:25 +0000 (11:17 +0200)]
Implement automaton simplification.
Kim Nguyễn [Wed, 12 Oct 2016 15:44:32 +0000 (17:44 +0200)]
Simplify the automaton encoding a bit (remove redundant predicates in formulae).
Kim Nguyễn [Wed, 12 Oct 2016 11:39:07 +0000 (13:39 +0200)]
Refactor pretty printing of transitions and fix some depracated function uses.
Kim Nguyễn [Wed, 12 Oct 2016 08:41:52 +0000 (10:41 +0200)]
add .merlin file.
Kim Nguyễn [Wed, 12 Oct 2016 08:41:26 +0000 (10:41 +0200)]
* Seal the representation of states
* Compile with -principal -warning-error @3
Kim Nguyễn [Tue, 29 Apr 2014 07:45:26 +0000 (09:45 +0200)]
Revert the integration of menhir for the time being.
Revert "Cherry pick use of menhir features from branch feature/menhir."
Revert "Further simplify Remakefile. Remove some inefficiency in module dependency checking script."
Revert "Remove passing $NATIVE on the remake command line of every target, since variable contents are propagated."
Revert "Modify configure.in and Remakefile.in to use menhir instead of ocamlyacc."
Kim Nguyễn [Mon, 17 Mar 2014 13:08:57 +0000 (14:08 +0100)]
Cherry pick use of menhir features from branch feature/menhir.
Work around a bug in menhir that generates code with the 'lexer' identifier which in turn makes ulex syntax extension choke.
Kim Nguyễn [Mon, 3 Mar 2014 23:21:26 +0000 (00:21 +0100)]
Further simplify Remakefile. Remove some inefficiency in module dependency checking script.
Kim Nguyễn [Mon, 3 Mar 2014 18:44:50 +0000 (19:44 +0100)]
Remove passing $NATIVE on the remake command line of every target, since variable contents are propagated.
Kim Nguyễn [Mon, 3 Mar 2014 16:00:05 +0000 (17:00 +0100)]
Modify configure.in and Remakefile.in to use menhir instead of ocamlyacc.
(This only modify the build process, not the parser itself, so the parser is
still a plain ocamlyacc file).
Kim Nguyễn [Mon, 3 Mar 2014 16:05:01 +0000 (17:05 +0100)]
Update to remake version 0.11 (support for .PHONY targets).
Kim Nguyễn [Tue, 21 Jan 2014 13:10:01 +0000 (14:10 +0100)]
Cosmetic changes (whitespaces and indentation)
Kim Nguyễn [Sat, 11 Jan 2014 20:56:59 +0000 (21:56 +0100)]
Refactor the statistics gathering code in run.ml
Kim Nguyễn [Sat, 11 Jan 2014 17:22:16 +0000 (18:22 +0100)]
Implement subtree-skipping optimisation (a one liner, really ~_~) that skips a whole subtree during the topdown phase when some states had to be proven but none could.
Kim Nguyễn [Sat, 11 Jan 2014 13:38:27 +0000 (14:38 +0100)]
Perform selection of nodes during the last run instead of performing an extra traversal.
Kim Nguyễn [Sat, 11 Jan 2014 12:13:59 +0000 (13:13 +0100)]
Change the interface of node_list (fully imperative now)
Kim Nguyễn [Fri, 10 Jan 2014 23:34:11 +0000 (00:34 +0100)]
Abstract result sets beind a Node_list interface.
Kim Nguyễn [Tue, 7 Jan 2014 16:06:53 +0000 (17:06 +0100)]
Fix a bug in ocaml build script (echo -n is not supported on OSX,
use /bin/echo instead)
Kim Nguyễn [Mon, 9 Dec 2013 09:57:59 +0000 (10:57 +0100)]
Refactor the tracing code, store the whole tree structure in a javascript array and handle it from the javascript side.
Kim Nguyễn [Sun, 8 Dec 2013 16:20:37 +0000 (17:20 +0100)]
Cosmetic changes (whitespaces) and add comments at the top of the .str files to load the correct emacs-mode when editing.
Kim Nguyễn [Sun, 8 Dec 2013 10:31:26 +0000 (11:31 +0100)]
Update to latest master of remake.
Add a workaround to silence the linker warning when building remake in the configure script.
Kim Nguyễn [Sun, 8 Dec 2013 09:55:54 +0000 (10:55 +0100)]
Refactor HTML Tracing to not depend on external files (style, javascript). Add a general facility to turn a file into an OCaml string. The content of file.ml.str is turned into let content = "..." in a file file.ml.
Kim Nguyễn [Sun, 8 Dec 2013 09:54:54 +0000 (10:54 +0100)]
Refactor the run module, moving out of the Make functor everything that can be moved. Slightly improve the cache module by avoiding one comparison during find on some cases and remove manual call to Gc.compact in main, since it does not seem to help.
Kim Nguyễn [Fri, 6 Dec 2013 15:09:27 +0000 (16:09 +0100)]
Resurect the HTML trace. Now generates a single HTML file containing the SVG.
Kim Nguyễn [Tue, 3 Dec 2013 23:02:02 +0000 (00:02 +0100)]
Rename xmark test files so that the name order respects the size order.
Fix the gen_xmark script.
Kim Nguyễn [Tue, 3 Dec 2013 22:59:24 +0000 (23:59 +0100)]
Fix a bug in the test-complexity script and add more test cases.
Kim Nguyễn [Tue, 3 Dec 2013 22:57:12 +0000 (23:57 +0100)]
Speed-up the run function by keeping only the set of node to be satified for each node.
Kim Nguyễn [Mon, 2 Dec 2013 21:30:43 +0000 (22:30 +0100)]
WIP
Kim Nguyễn [Sun, 1 Dec 2013 20:14:54 +0000 (21:14 +0100)]
Split the formula cache into a top-down and bottom-up cache.
Kim Nguyễn [Sun, 1 Dec 2013 12:18:59 +0000 (13:18 +0100)]
Remove some unneeded code that was slowing down the run function.
Kim Nguyễn [Sun, 1 Dec 2013 11:05:40 +0000 (12:05 +0100)]
Add missing tests for xmark_0.xml file.
Kim Nguyễn [Sun, 1 Dec 2013 08:20:06 +0000 (09:20 +0100)]
Add the results of reference implementations back.
Kim Nguyễn [Sat, 30 Nov 2013 21:32:17 +0000 (22:32 +0100)]
Fix typos int the test file generation script.
Kim Nguyễn [Sat, 30 Nov 2013 21:30:05 +0000 (22:30 +0100)]
Add generated test files to .gitignore
Kim Nguyễn [Sat, 30 Nov 2013 21:29:04 +0000 (22:29 +0100)]
Refactor the testing infrastructure.
Kim Nguyễn [Sat, 30 Nov 2013 18:27:49 +0000 (19:27 +0100)]
Refine the run to have a different set of states to satisfy while going td/bu.
Kim Nguyễn [Sat, 30 Nov 2013 12:19:03 +0000 (13:19 +0100)]
Fix a bug in the build script that was causing some .cmo files to have a false dependency on .cmx files.
Kim Nguyễn [Sat, 30 Nov 2013 08:27:36 +0000 (09:27 +0100)]
Replace "unsafe" function tempnam by custom code.
Kim Nguyễn [Sat, 30 Nov 2013 08:25:47 +0000 (09:25 +0100)]
Make remake print "Entering/Leaving directory `foo'" if it changes the current working dir.
Kim Nguyễn [Thu, 28 Nov 2013 22:21:54 +0000 (23:21 +0100)]
Add a target to run tests with the bytecode version of the program.
Kim Nguyễn [Thu, 28 Nov 2013 20:32:49 +0000 (21:32 +0100)]
Update to master version of remake.
Kim Nguyễn [Mon, 25 Nov 2013 20:39:46 +0000 (21:39 +0100)]
Cosmetic changes (truncate long lines, remove trailing spaces…)
Kim Nguyễn [Sun, 24 Nov 2013 21:20:12 +0000 (22:20 +0100)]
Implement the ranked automata evaluation to guarantee a O(|D|x|Q|)
worst case complexity. The states of an automaton are given a rank (an
integer) such that if rank(q) = i, then state q can be satisfied
during run i at the latest. The maximum rank of a state is bounded by
the number of "bi-directional" states, that is, the number of states
which depends at the same time on a state upward and on another state
downard. Therefore, the rank is at most |Q|. For the moment, we
evaluate state [q] *only* during run i. This implies the O(|D|x|Q|)
overal complexity but also means we loose a chance to discard (or
accept) [q] early. A heuristic could improve that.
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.