Requirements for compilation:
build-essential flex bison cmake libboost-all-dev
For Ubuntu 19.10 (ssh keys must be already configured for github):
# install prerequisites
sudo apt update
sudo apt upgrade
sudo apt install build-essential flex bison cmake libboost-all-dev
# get aalwines (P-Rex v2) and compile
git clone [email protected]:DEIS-Tools/aalwines.git
cd aalwines
mkdir build
cd build
cmake ..
make
export MOPED_PATH=`pwd`/../bin/moped
# binary will be in build/binOption for static linkage -> binary will not need libboost and other libs installed on target system:
cmake -DAALWINES_BuildBundle=ON ..This will run queryfile query.txt over the network defined in the P-Rex data files, using moped as external engine and producing a trace:
cd bin
./aalwines --topology ../../../P-Rex/res/nestable/topo.xml --routing ../../../P-Rex/res/nestable/routing.xml -e 1 -q query.txt -tAn example query.txt (syntax see below):
<.> .* [s2#.] .* <.> 0 OVER
<.> .* [s2#.] .* <.> 0 UNDER
will produce following output:
{
"network-parsing-time":0.0192828, "query-parsing-time":0.0011643,
"answers":{
"Q1" : {
"result":true,
"reduction":[1179, 1179],
"trace":[
{"router":"s2","stack":["10"]},
{"pre":"10","rule":{"weight":0, "via":"s4"}},
{"router":"s4","stack":["10"]}
],
"compilation-time":0.0387264,
"reduction-time":1.07e-05,
"verification-time":0.0340714
},
"Q2" : {
"result":true,
"reduction":[1179, 1179],
"trace":[
{"router":"s2","stack":["10"]},
{"pre":"10","rule":{"weight":0, "via":"s4"}},
{"router":"s4","stack":["10"]}
],
"compilation-time":0.038969,
"reduction-time":8.4e-06,
"verification-time":0.0349733
}
}}A query file contains one or more queries. They can be separated by space or new line. Each query consists out of following parts:
<preCondition> path <postCondition> linkFailures mode
| part | type | description |
|---|---|---|
preCondition |
regex-list | labels before first router |
path |
regex-list | path through the network |
postCondition |
regex-list | labels after last router |
linkFailures |
number | maximum failed links |
mode |
enum | simulation mode: one out of OVER, UNDER, DUAL, EXACT |
The type regex-list is a space separated list of regular expressions (syntax see below).
For preCondition and postCondition it defines the labels on the stack of the packet. Packets must have at least 1 label when entering or leaving the network. For path it defines the interfaces(routers) the packet must, can or must not follow.
The mode can be OVER or UNDER. DUAL is a combination of OVER and UNDER. EXACT is not supported yet.
Every regular expression in the regex-list is built out of following components:
| syntax | description |
|---|---|
regex & regex |
AND: both regex must be fulfilled |
regex | regex |
OR: one or both regex must be fulfilled |
. |
matches everything |
regex+ |
multiple: regex must match once or multiple times |
regex* |
optional multiple: regex must match zero, one or multiple times |
regex? |
optional: regex must match zero or one time |
[atom-list] |
matches the atom_list (see below) |
[^atom-list] |
matches everything except the atom_list |
ip |
matches any ip address |
mpls |
matches any non-sticky mpls label |
smpls |
matches any sticky mpls label |
(regex-list) |
must match the given sub regex-list |
The atom-list contains a comma separated list of atoms (for path) or labels(for preCondition and postCondition).
Only labels are allowed in preCondition and postCondition and only Atoms in the path.
The semantics of an atom-list is that of union (OR) and the negation-symbol ^ is intepreted as complement of the following atom-list.
An atom defines a hop between routers via their exit and entry interfaces. An atom-list with one entry looks like:
[exit_if#entry_if]
with multiple entries the syntax is:
[exit_if1#entry_if1,exit_if2#entry_if2,...]
Following possibilities can be used for entry_if and exit_if:
| syntax | description |
|---|---|
| name | the router name (matches any interface of that router) |
name.name |
specific interface of router |
. |
any interface on any router |
name itself can be either an identifier (starting with a character; defining an exact interface) or a literal (a double-quoted regular expression matching interfaces "regex").
The regex-matching of name is implemented via boost::basic_regex and follows this semantics.
The syntax of a list with labels is:
| syntax | description |
|---|---|
[$label] |
A sticky label. Can be used with all following types |
[label1,label2] |
A list of labels. Can be used with all following types |
[number] |
A mpls label with number |
[number/mask] |
A range of mpls labels, specified by number and a mask in bits |
[ip] |
An ip label. Can be an ipv4 or an ipv6 address |
[ip/mask] |
An ip network. An ipv4 or an ipv6 address together with a mask in bits |