QuantiS permits the evaluation of Quantitative Specifications over finite words. The specification is done via some weighted hybrid expressions (with a syntax close to usual regular expressions). The command line tool permits to evaluate such a specification over a given word, by using automata techniques.
The tool is available for Unix. Although not tested, it should also work on Windows.
Source code and binaries: QuantiS-1.0.tar.gz
The archive already contains the executable file QuantiS in the /bin directory. Please check first if it is executable on your system. If it is not the case, you may follow these instructions to compile it by yourself.
The installation requires the use of OCaml (tested under Objective Caml version 3.12.1). In the /src directory, a makefile (using ocamlbuild) compiles all the files automatically: simply type
makein a terminal. It produces the executable file eval in the /bin directory, that you may use to evaluate an expression over a word. Make sure to add this path to the PATH variable to use freely the executables
export PATH=$PATH:/path/to/QuantiS/bin/
In the current version 1.0, you may use the tool as follows:
QuantiS -expr '(x!((2..->)^*).->)^*' -word 'aaa'This launches the evaluation of the hybrid weighted expression $(x!((2 \cdot{\rightarrow})^\star)\cdot{\rightarrow})^\star$ over the word $aaa$, resulting in the weight $16$. You may also use the option
-timerto use a timer.
The formal syntax used for hybrid weighted expressions over words is the following: \[E ::= s \mid \alpha \mid {\rightarrow} \mid {\leftarrow} \mid E+E \mid E\cdot E \mid E^+\mid E^\star \mid x!E\] where $s$ is a weight in $\mathbb R^+\cup\{+\infty\}$, $x$ is a variable and $\alpha$ is a test formula defined by the grammar \[\alpha ::= \top \mid \mathrm{begin}\mid \mathrm{end} \mid a? \mid {\rightarrow}? \mid {\leftarrow}? \mid \lnot \alpha\mid \alpha\lor\alpha\mid \alpha\land\alpha\] with $a$ a letter from a finite alphabet. For the purpose of the tool, and for simplicity, we restrict the alphabet to be the letters from $a$ to $w$, whereas variables must be in the range $x$ to $z$. All the expressions may be written in plain text, since a lexer is included in the implementation of the tool. However, please do remember the following conventions:
You may find in the /examples directory a shell script tests.sh with some examples of usage of this executable. Simply lauch the script in a terminal. (If you didn't export manually the path to the PATH variable, the script does it for you, at the condition that you launch it from the directory itself.)