update verigraph

JIRA: PARSER-154

code optimizations about graph manipulation and formula generation.

Change-Id: Idebef19b128281aa2bc40d1aeab6e208c7ddd93d
Signed-off-by: serena.spinoso <serena.spinoso@polito.it>

5 files changed, 113 insertions, 14 deletions

diff --git a/docs/developer/design/images/verigraph.png b/docs/developer/design/images/verigraph.png
index dfcd586..617d2d5 100644
--- a/docs/developer/design/images/verigraph.png
+++ b/docs/developer/design/images/verigraph.png
diff --git a/docs/developer/design/verigraph.rst b/docs/developer/design/verigraph.rst
index 1362e23..a2e1508 100644
--- a/docs/developer/design/verigraph.rst
+++ b/docs/developer/design/verigraph.rst
@@ -26,24 +26,25 @@ Architecture
 VeriGraph exploits two sub-modules:
 
 - **Z3**, the SMT solver developed by Microsoft
-- **Neo4JManger**, a module that can store service graphs into a *Neo4J* graph-oriented database
+- **Neo4J**, a Java-based graph-oriented database
 
-Neo4JManager can also extract from a service graph all the VNF chains that are
-relevant for checking the reachability properties of that graph.
+The Neo4J database is used for service graph manipulation and to extract from a
+service graph all the VNF chains that are relevant for checking the reachability
+properties of that graph.
 
 How the tool works
 ------------------
 VeriGraph accepts JSON service graph descriptions that include endpoints, VNF instances, logical
 directed links connecting them, and VNF configurations.
 
-When VeriGraph receives a service graph and a reachability property to verify, it forwards the graph
-to Neo4JManager and asks Neo4JManager to extract the chains that connect the nodes addressed by the
-property to be checked. For each one of these chains, VeriGraph builds a set of first order logic
-formulas that represent a mathematical model of the forwarding behavior of the chain.
-This model takes into account the forwarding behavior of the links and of the VNFs included in the chain,
-taking into consideration their configurations. If the formulas that make up the model are satisfiable,
-this means that it is possible for a packet to traverse the chain from one end to the other.
-VeriGraph passes this model to Z3 which checks its satisfiability.
+When VeriGraph receives a service graph and a reachability property to verify, it saves the graph
+into Neo4J and it extracts the chains that connect the nodes addressed by the property to be
+checked. For each one of these chains, VeriGraph builds a set of first order logic formulas that
+represent a mathematical model of the forwarding behavior of the chain.
+This model takes into account the forwarding behavior of the links and of the VNFs included in the
+chain, taking into consideration their configurations. If the formulas that make up the model are
+satisfiable, this means that it is possible for a packet to traverse the chain from one end to the
+other. VeriGraph passes this model to Z3 which checks its satisfiability.
 Based on the satisfiability result of the formulas that model the different paths, VeriGraph finally
 derives the overall result (reachability property satisfied or not).
 
diff --git a/docs/release/installation/installation.instruction.rst b/docs/release/installation/installation.instruction.rst
index 323fd4a..b399038 100644
--- a/docs/release/installation/installation.instruction.rst
+++ b/docs/release/installation/installation.instruction.rst
@@ -111,6 +111,7 @@ Parser verigraph installation
 In the present release, verigraph requires that the following software is also installed:
 
 - Java 1.8 (with javac compiler)
+- Apache Ant 1.9
 - Apache Tomcat 8
 - Microsoft Z3 (https://github.com/Z3Prover/bin/tree/master/releases)
 - Neo4J (https://neo4j.org)
@@ -129,8 +130,86 @@ Step 2: Go to the verigraph directory.
 
    cd parser/verigraph
 
-Step3: Follow the instructions in README.rst for downloading verigraph
-dependencies and for installing verigraph.
+Step3: Set up the execution environment, based on your operating system.
+
+*VeriGraph deployment on Apache Tomcat (Windows)*:
+
+-  set JAVA HOME environment variable to where you installed the jdk
+   (e.g. ``C:\Program Files\Java\jdk1.8.XYY``);
+-  set CATALINA HOME ambient variable to the directory where you
+   installed Apache (e.g.
+   ``C:\Program Files\Java\apache-tomcat-8.0.30``);
+-  open the file ``%CATALINA_HOME%\conf\tomcat-users.xml`` and under the ``tomcat-users`` tag place,
+   initialize an user with roles "tomcat, manager-gui, manager-script". An example is the following
+   content: ``xml   <role rolename="tomcat"/>   <role rolename="role1"/>   <user username="tomcat"
+   password="tomcat" roles="tomcat,manager-gui"/>   <user username="both" password="tomcat"
+   roles="tomcat,role1"/>   <user username="role1" password="tomcat" roles="role1"/>``
+-  edit the "to\_be\_defined" fields in tomcat-build.xml with the username and password previously
+   configured in Tomcat(e.g. ``name="tomcatUsername" value="tomcat"`` and ``name="tomcatPassword"
+   value="tomcat"`` the values set in 'tomcat-users'). Set ``server.location`` property to the
+   directory where you installed Apache (e.g. ``C:\Program Files\Java\apache-tomcat-8.0.30``);
+
+*VeriGraph deployment on Apache Tomcat (Unix)*:
+
+- ``sudo nano ~/.bashrc``
+-  set a few environment variables by paste the following content at the end of the file
+   ``export CATALINA_HOME='/path/to/apache/tomcat/folder'``
+   ``export JRE_HOME='/path/to/jdk/folder'``
+   ``export JDK_HOME='/path/to/jdk/folder'``
+- ``exec bash``
+-  open the file ``$CATALINA_HOME\conf\tomcat-users.xml`` and under
+   the ``tomcat-users`` tag place, initialize an user with roles
+   "tomcat, manager-gui, manager-script". An example is the following content:
+   ``xml <role rolename="tomcat"/>   <role rolename="role1"/>   <user username="tomcat"
+   password="tomcat" roles="tomcat,manager-gui"/>   <user username="both" password="tomcat"
+   roles="tomcat,role1"/>   <user username="role1" password="tomcat" roles="role1"/>``
+-  edit the "to\_be\_defined" fields in tomcat-build.xml with the
+   username and password previously configured in Tomcat(e.g. ``name="tomcatUsername"
+   value="tomcat"`` and ``name="tomcatPassword" value="tomcat"`` the values set in 'tomcat-users').
+   Set ``server.location`` property to the directory where you installed Apache
+   (e.g. ``C:\Program Files\Java\apache-tomcat-8.0.30``);
+
+
+
+Step4a: Deploy Verigraph in Tomcat.
+
+.. code-block:: bash
+
+   ant -f build.xml deployWS
+
+Use the Ant script build.xml to manage Verigraph webservice with the following targets:
+
+-  generate-war: it generates the war file;
+-  generate-binding: it generates the JAXB classes from the XML Schema file xml\_components.xsd;
+-  start-tomcat : it starts the Apache Tomcat;
+-  deployWS: it deploys the verigraph.war file contained in
+   verigraph/war folder;
+-  startWS: it starts the webservice;
+-  run-test: it runs the tests in tester folder. It is possible to
+   choose the iterations number for each verification request by
+   launching the test with "-Diteration=n run-test" where n is the
+   number of iterations you want;
+-  stopWS: it stops the webservice;
+-  undeployWS: it undeploys the webservice from Apache Tomcat;
+-  stop-tomcat: it stops Apache Tomcat.
+
+Step4b: Deploy Verigraph with gRPC interface.
+
+.. code-block:: bash
+
+   ant -f build.xml generate-binding
+   ant -f gRPC-build.xml run-server
+
+Use the Ant script gRPC-build.xml to manage Verigraph with the following targets:
+
+- build: compile the program;
+- run: run both client and server;
+- run-client : run only client;
+- run-server : run only server;
+- run-test : launch all tests that are present in the package;
+
+
+
 
 
 Parser apigateway Installation
diff --git a/docs/release/userguide/feature.userguide.rst b/docs/release/userguide/feature.userguide.rst
index 1113118..61063c2 100644
--- a/docs/release/userguide/feature.userguide.rst
+++ b/docs/release/userguide/feature.userguide.rst
@@ -194,5 +194,5 @@ to create a service graph using the gRPC interface and to trigger the verificati
 .. code-block:: bash
 
       cd parser/verigraph
-      #Client souce code in ``parser/verigraph/src/main/it/polito/grpc/Client.java``
+      #Client souce code in ``parser/verigraph/src/it/polito/verigraph/grpc/client/Client.java``
       ant -f buildVeriGraph_gRPC.xml run-client
diff --git a/docs/testing/testusage.rst b/docs/testing/testusage.rst
index 36b9c00..7bc9b12 100644
--- a/docs/testing/testusage.rst
+++ b/docs/testing/testusage.rst
@@ -58,6 +58,11 @@ Parser VeriGraph test usage
 VeriGraph is accessible via both a RESTfull API and a gRPC interface.
 
 **RESTful API**
+In order to run the automatic testing script, you need the
+following dependencies installed on your python distribution:
+
+- "requests" python package -> http://docs.python-requests.org/en/master/
+- "jsonschema" python package -> https://pypi.python.org/pypi/jsonschema
 
 1. Run the Python tester
 
@@ -66,6 +71,20 @@ VeriGraph is accessible via both a RESTfull API and a gRPC interface.
       cd parser/verigraph/tester
       python test.py
 
+2. Run many times (i.e. n-times) each test-case with ant script
+
+.. code-block:: bash
+
+      cd parser/verigraph
+      ant -f build.xml run-test -Diteration=n
+
+2. Run many times (i.e. n-times) each test-case by command line
+
+.. code-block:: bash
+
+      cd parser/verigraph
+      python test.py -iteration n
+
 **gRPC API**
 
 1. Compile the code