QuAK is an open source C++ library that helps automate the analysis of quantitative automata.
Currently, QuAK supports the classes of quantitative automata with the following value functions:
Let
- Check if
$\mathcal{A}$ is non-empty with respect to$v$ . - Check if
$\mathcal{A}$ is universal with respect to$v$ . - Check if
$\mathcal{A}$ is included in$\mathcal{B}$ . - Check if
$\mathcal{A}$ defines a constant function. - Check if
$\mathcal{A}$ defines a safety property. - Check if
$\mathcal{A}$ defines a liveness property. - Compute the top value
$\top$ of$\mathcal{A}$ . - Compute the bottom value
$\bot$ of$\mathcal{A}$ . - Compute the safety closure of
$\mathcal{A}$ . - Compute the safety-liveness decomposition of
$\mathcal{A}$ . - Construct and execute a monitor for
$\mathcal{A}$ .
QuAK has no external dependencies. The only requirement is to have a C++ compiler that supports the C++17 standard or newer.
The easiest way to build QuAK is to use CMake + make:
On Ubuntu, you can install CMake and Make with the following command:
apt-get install make cmake
Then you can compile QuAK:
cmake . -DCMAKE_BUILD_TYPE=Release
make -j4
For debug builds, use Debug
instead of Release
. You can tweak compile time
options that enable the optimization of algorithms: use
-DENABLE_SCC_SEARCH_OPT=OFF
to turn off an SCC-based optimization of deciding
language inclusion (and other problems where the inclusion algorithm is used as a subroutine).
To compile the code with link-time (i.e., inter-procedural) optimizations,
use the option -DENABLE_IPO=ON
.
Once compiled, you can run tests with calling make test
.
First build VAMOS. Then run cmake with these parameters:
cmake . -Dvamos_DIR=/path/to/vamos/directory
make -j4
QuAK reads and constructs automata from text files. Each automata is represented as a list of transitions of the following format:
a : v, q -> p
which encodes a transition from state
The initial state of the input automaton is the source state of the first transition in its text file.
Important: QuAK requires that its input automata are complete (a.k.a. total), i.e., for every state
To use the library in your program, use the following directive:
#include "FORKLIFT/inclusion.h"
#include "Automaton.h"
#include "Monitor.h"
For a sample program that puts together the demonstrations below, see examples/sampleProgram.cpp.
Below, we consider two
To construct an automaton from a file, use the following template:
Automaton* A = new Automaton("A.txt");
The value function is unspecified during construction, but it needs to be passed as a parameter to the functions below.
To check the non-emptiness of
bool flag = A->isNonEmpty(Val, v);
To check the universality of
bool flag = A->isUniversal(Val, v);
To check the inclusion of
bool flag = A->isIncludedIn(B, Val, booleanized);
where booleanized determines which inclusion algorithms is called. If booleanized is false, then our quantitative extension of the antichain algorithm is used. If booleanized is true, then the standard inclusion algorithm (repeatedly booleanizing the quantitative automaton and calling the boolean antichain algorithm) is used. By default, booleanized is set to false.
To check if
bool flag = A->isConstant(Val);
To check if
bool flag = A->isSafe(Val);
To check if
bool flag = A->isLive(Val);
To compute the top value of
weight_t top = A->getTopValue(Val);
To compute the bottom value of
weight_t top = A->getBotValue(Val);
To construct the safety closure of
Automaton* safe_A = safetyClosure(A, Val);
For the safety component of the decomposition, use the safety closure construction above.
To construct the liveness component of the decomposition of
Automaton* live_A = livenessComponent_deterministic(A, Val);
QuAK can contsruct monitors from deterministic automata by either reading them from a file or copying an automaton object:
Monitor* M = new Monitor("A.txt", Val);
Monitor* M = new Monitor(A, Val);
where
The monitor updates its state by reading a letter of type std::string and returning the current value:
weight_t t = M->next(letter);
For example, a monitor can process a word file as follows:
std::ifstream stream("samples/wordfile.txt");
std::string symbol;
while (stream) {
stream >> symbol;
std::cout << symbol << " -> " << M->next(symbol) << "\n" << std::flush;
}
To use the tool directly, simply compile and follow the instructions below.
Usage: ./quak [-cputime] [-v] [-d] automaton-file [ACTION ACTION ...]
Where ACTIONs are the following, with VALF = <Inf | Sup | LimInf | LimSup | LimSupAvg | LimInfAvg>:
stats
dump
empty VALF <weight>
non-empty VALF <weight>
universal VALF <weight>
constant VALF
safe VALF
live VALF
isIncluded VALF automaton2-file
isIncludedBool VALF automaton2-file
monitor <Inf | Sup | Avg> word-file
monitor-vamos <Inf | Sup | Avg> shmkey
The commands stats prints the size of the automaton and dump prints the automaton. The remaining commands implement the decision procedures and monitoring algorithms as expected. For monitoring, the word files must contain one symbol per line. Use the option -cputime to print the running time, -v to print the input size, and -d to print the automaton. An example is given below.
./quak -cputime -d A.txt safe LimInfAvg
Cputime of building the automaton: 3 ms
automaton (A.txt):
alphabet (2):
0 -> a
1 -> b
weights (5):
0 -> -9.545000
1 -> -5.077000
2 -> 0.634000
3 -> 1.100000
4 -> 6.122000
MIN = -9.545000
MAX = 6.122000
states (2):
0 -> q0, scc: 0
1 -> q1, scc: -1
INITIAL = q0
SCCs (1):
q0
edges (5):
a : -9.545, q0 -> q0
b : 1.1, q0 -> q0
a : 0.634, q1 -> q1
a : 6.122, q1 -> q0
b : -5.077, q1 -> q0
----------
isSafe(LimInfAvg) = 0
Cputime: 4 ms
----------