From: Kim Nguyễn <kn@lri.fr>
Date: Sun, 24 Nov 2013 21:20:12 +0000 (+0100)
Subject: Implement the ranked automata evaluation to guarantee a O(|D|x|Q|)
X-Git-Tag: v0.1~32
X-Git-Url: http://git.nguyen.vg/gitweb/?a=commitdiff_plain;h=78d247dc5e6d5e64a4ab848702c23ce81b6fc615;hp=78d247dc5e6d5e64a4ab848702c23ce81b6fc615;p=tatoo.git

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.
---