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 libfl-dev
# get aalwines and compile
git clone [email protected]:DEIS-Tools/aalwines.git
cd aalwines
mkdir build
cd build
cmake -DCMAKE_BUILD_TYPE=Release ..
make
# binary will be in build/binOption for pseudo static linkage -> binary will not need libboost and other libs installed on target system:
cmake -DAALWINES_BuildBundle=ON -DCMAKE_BUILD_TYPE=Release ..This will run queryfile query.txt and weightfile weight.json over the network defined in the AalWiNes JSON network file, using Post* implementation as engine and producing a trace:
cd bin
./aalwines --input ../../example_net/Agis-network.json -w ../../example_net/Agis-weight.json -q ../../example_net/Agis-query.q -t -e 1An example query.txt (syntax see below):
<.> [.#Stockton] .* [Santa_Clara#.] <.> 0 DUAL
<.> [.#Chicago] [^.#Los_Angeles]* [Santa_Clara#.] <.> 1 DUAL
An example weight.json (syntax see below):
[
[
{"atom": "tunnels"}
],
[
{"atom": "local_failures"},
{"atom": "hops", "factor": 2}
]
]
will produce following output:
{
"network-parsing-time":0.661911, "query-parsing-time":0.0021034,
"answers":{
"Q1" : {
"result": true,
"engine": "Post*",
"mode": "OVER",
"reduction":[70918, 70918],
"trace-weight": [0, 4],
"trace":[
{"router":"Stockton","stack":["1599^"]},
{"ingoing":"iStockton","pre":"1599^","rule":{"weight":0, "via":"Santa_Clara", "ops":[{"swap":"1600"}]}, "priority-weight": ["0", "2"]},
{"router":"Santa_Clara","stack":["1600"]},
{"ingoing":"Stockton","pre":"1600","rule":{"weight":0, "via":"Los_Angeles", "ops":[{"swap":"1601"}]}, "priority-weight": ["0", "2"]},
{"router":"Los_Angeles","stack":["1601"]}
],
"compilation-time":0.303446,
"reduction-time":0.0012157,
"verification-time":1.24293
},
"Q2" : {
"result": true,
"engine": "Post*",
"mode": "OVER",
"reduction":[129519, 129519],
"trace-weight": [1, 9],
"trace":[
{"router":"Chicago","stack":["2922"]},
{"ingoing":"St_Louis","pre":"2922","rule":{"weight":1, "via":"Seattle", "ops":[{"swap":"2923"}, {"push":"3452"}]}, "priority-weight": ["1", "3"]},
{"router":"Seattle","stack":["3452","2923"]},
{"ingoing":"Chicago","pre":"3452","rule":{"weight":0, "via":"San_Francisco", "ops":[{"swap":"3451"}]}, "priority-weight": ["0", "2"]},
{"router":"San_Francisco","stack":["3451","2923"]},
{"ingoing":"Seattle","pre":"3451","rule":{"weight":0, "via":"Santa_Clara", "ops":[{"swap":"3450"}]}, "priority-weight": ["0", "2"]},
{"router":"Santa_Clara","stack":["3450","2923"]},
{"ingoing":"San_Francisco","pre":"3450","rule":{"weight":0, "via":"Los_Angeles", "ops":["pop"]}, "priority-weight": ["0", "2"]},
{"router":"Los_Angeles","stack":["2923"]}
],
"compilation-time":0.484016,
"reduction-time":0.0026069,
"verification-time":2.01965
}
}
}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, 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 currently only be OVER. EXACT is not supported yet.
A weight file contains a priority in the outer array. The inner array contains the linear combination of atoms.
[
[
{"atom": ATOM, "factor": NUM},
...
],
...
]
ATOM = {links, hops, distance, local_failures, tunnels, }
NUM = {0,1,2,...} factor is optional and NUM default is 1.
The different priority groups, of linear combinations, represent the order of which the weights are compared. The second priority group will be considered if two similar weighted traces in the first linear combination are equal.
links minimize the number of links in the trace.
hops minimize the number of hops (not counting links that are self-loops) in the trace.
distance minimize the accumulated distance between routers estimated from router coordinates.
local_failures minimize the sum of locally counted failed links at each router on the trace. This number may be higher than the global number of failed links in the case of loops, since some links may be counted twice.
tunnels minimize the number of push operations in the trace.
Every regular expression in the regex-list is built out of following components:
| syntax | description |
|---|---|
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 |
(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 |
|---|---|
[label1,label2] |
A list of labels. Can be used with all following types |
[number] |
A mpls label with number |