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>

7 files changed, 369 insertions, 613 deletions

diff --git a/verigraph/tester/testcases/test_budapest_sap1_webserver_sat.json b/verigraph/tester/testcases/test_budapest_sap1_webserver_sat.json
index 62b4eb5..6a64eea 100644
--- a/verigraph/tester/testcases/test_budapest_sap1_webserver_sat.json
+++ b/verigraph/tester/testcases/test_budapest_sap1_webserver_sat.json
@@ -1,122 +1,128 @@
 {
-   "id":6,
-   "name":"budapest_test_case_sat",
-   "description":"This test case verifies budapest scenario, chain sap1->webserver1",
-   "policy_url_parameters":"?type=reachability&source=sap1&destination=webserver1",
-   "result":"SAT",
-   "graph": {
-      "nodes":[
-         {
-            "neighbours":[
-               {
-                  "name":"webserver1"
-               },
-               {
-                  "name":"nat"
-               }
-            ],
-            "configuration":[
-               {
-                  "ip_sap1":"webserver1"
-               }
-            ],
-            "name":"fw",
-            "functional_type":"firewall"
-         },
-         {
-            "neighbours":[
-               {
-                  "name":"sap3"
-               },
-               {
-                  "name":"fw"
-               }
-            ],
-            "name":"webserver1",
-            "functional_type":"webserver"
-         },
-         {
-            "neighbours":[
-               {
-                  "name":"sap1"
-               },
-               {
-                  "name":"dpi"
-               },
-               {
-                  "name":"fw"
-               }
-            ],
-            "configuration":[
-               "sap1",
-               "sap2"
-            ],
-            "name":"nat",
-            "functional_type":"nat"
-         },
-         {
-            "neighbours":[
-               {
-                  "name":"sap2"
-               }
-            ],
-            "configuration":[
-               "drug"
-            ],
-            "name":"dpi",
-            "functional_type":"dpi"
-         },
-         {
-            "neighbours":[
-               {
-                  "name":"nat"
-               }
-            ],
-            "configuration":[
-               {
-                  "url":"www.facebook.com",
-                  "body":"cats",
-                  "destination":"webserver1",
-                  "protocol":"HTTP_REQUEST"
-               }
-            ],
-            "name":"sap2",
-            "functional_type":"endhost"
-         },
-         {
-            "neighbours":[
-               {
-                  "name":"nat"
-               }
-            ],
-            "configuration":[
-               {  
-                  "url":"www.facebook.com",
-                  "body":"cats",
-                  "destination":"webserver1",
-                  "protocol":"HTTP_REQUEST"
-               }
-            ],
-            "name":"sap1",
-            "functional_type":"endhost"
-         },
-         {
-            "neighbours":[
-               {
-                  "name":"webserver1"
-               }
-            ],
-            "configuration":[
-               {
-                  "url":"www.facebook.com",
-                  "body":"cats",
-                  "destination":"webserver1",
-                  "protocol":"HTTP_REQUEST"
-               }
-            ],
-            "name":"sap3",
-            "functional_type":"endhost"
-         }
-      ]
-   }
+    "id": 6,
+    "name": "budapest_test_case_sat",
+    "description": "This test case verifies budapest scenario, chain sap1->webserver1",
+    "policy_url_parameters": [
+        "?type=reachability&source=sap1&destination=webserver1",
+        "?type=reachability&source=sap3&destination=webserver1"
+    ],
+    "results": [
+        "SAT",
+        "SAT"
+    ],
+    "graph": {
+        "nodes": [
+            {
+                "neighbours": [
+                    {
+                        "name": "webserver1"
+                    },
+                    {
+                        "name": "nat"
+                    }
+                ],
+                "configuration": [
+                    {
+                        "sap1": "webserver1"
+                    }
+                ],
+                "name": "fw",
+                "functional_type": "firewall"
+            },
+            {
+                "neighbours": [
+                    {
+                        "name": "sap3"
+                    },
+                    {
+                        "name": "fw"
+                    }
+                ],
+                "name": "webserver1",
+                "functional_type": "webserver"
+            },
+            {
+                "neighbours": [
+                    {
+                        "name": "sap1"
+                    },
+                    {
+                        "name": "dpi"
+                    },
+                    {
+                        "name": "fw"
+                    }
+                ],
+                "configuration": [
+                    "sap1",
+                    "sap2"
+                ],
+                "name": "nat",
+                "functional_type": "nat"
+            },
+            {
+                "neighbours": [
+                    {
+                        "name": "sap2"
+                    }
+                ],
+                "configuration": [
+                    "drug"
+                ],
+                "name": "dpi",
+                "functional_type": "dpi"
+            },
+            {
+                "neighbours": [
+                    {
+                        "name": "nat"
+                    }
+                ],
+                "configuration": [
+                    {
+                        "url": "www.facebook.com",
+                        "body": "cats",
+                        "destination": "webserver1",
+                        "protocol": "HTTP_REQUEST"
+                    }
+                ],
+                "name": "sap2",
+                "functional_type": "endhost"
+            },
+            {
+                "neighbours": [
+                    {
+                        "name": "nat"
+                    }
+                ],
+                "configuration": [
+                    {
+                        "url": "www.facebook.com",
+                        "body": "cats",
+                        "destination": "webserver1",
+                        "protocol": "HTTP_REQUEST"
+                    }
+                ],
+                "name": "sap1",
+                "functional_type": "endhost"
+            },
+            {
+                "neighbours": [
+                    {
+                        "name": "webserver1"
+                    }
+                ],
+                "configuration": [
+                    {
+                        "url": "www.facebook.com",
+                        "body": "cats",
+                        "destination": "webserver1",
+                        "protocol": "HTTP_REQUEST"
+                    }
+                ],
+                "name": "sap3",
+                "functional_type": "endhost"
+            }
+        ]
+    }
 }
\ No newline at end of file
diff --git a/verigraph/tester/testcases/test_budapest_sap1_webserver_unsat.json b/verigraph/tester/testcases/test_budapest_sap1_webserver_unsat.json
index 211b310..e74194d 100644
--- a/verigraph/tester/testcases/test_budapest_sap1_webserver_unsat.json
+++ b/verigraph/tester/testcases/test_budapest_sap1_webserver_unsat.json
@@ -1,122 +1,126 @@
-{  
-   "id":7,
-   "name":"budapest_test_case_unsat",
-   "description":"This test case verifies budapest scenario, chain sap1->webserver1 with fw blocking",
-   "policy_url_parameters":"?type=reachability&source=sap1&destination=webserver1",
-   "result":"UNSAT",
-   "graph":{
-      "nodes":[
-         {
-            "neighbours":[
-               {
-                  "name":"webserver1"
-               },
-               {
-                  "name":"nat"
-               }
-            ],
-            "configuration":[
-               {
-                  "webserver1":"nat"
-               }
-            ],
-            "name":"fw",
-            "functional_type":"firewall"
-         },
-         {
-            "neighbours":[
-               {
-                  "name":"sap3"
-               },
-               {
-                  "name":"fw"
-               }
-            ],
-            "name":"webserver1",
-            "functional_type":"webserver"
-         },
-         {
-            "neighbours":[
-               {
-                  "name":"sap1"
-               },
-               {
-                  "name":"dpi"
-               },
-               {
-                  "name":"fw"
-               }
-            ],
-            "configuration":[
-               "sap1",
-               "sap2"
-            ],
-            "name":"nat",
-            "functional_type":"nat"
-         },
-         {
-            "neighbours":[
-               {
-                  "name":"sap2"
-               }
-            ],
-            "configuration":[
-               "drug"
-            ],
-            "name":"dpi",
-            "functional_type":"dpi"
-         },
-         {
-            "neighbours":[
-               {
-                  "name":"nat"
-               }
-            ],
-            "configuration":[
-               {
-                  "url":"www.facebook.com",
-                  "body":"cats",
-                  "destination":"webserver1",
-                  "protocol":"HTTP_REQUEST"
-               }
-            ],
-            "name":"sap2",
-            "functional_type":"endhost"
-         },
-         {
-            "neighbours":[
-               {
-                  "name":"nat"
-               }
-            ],
-            "configuration":[
-               {
-                  "url":"www.facebook.com",
-                  "body":"cats",
-                  "destination":"webserver1",
-                  "protocol":"HTTP_REQUEST"
-               }
-            ],
-            "name":"sap1",
-            "functional_type":"endhost"
-         },
-         {
-            "neighbours":[
-               {
-                  "name":"webserver1"
-               }
-            ],
-            "configuration":[
-               {
-                  "url":"www.facebook.com",
-                  "body":"cats",
-                  "destination":"webserver1",
-                  "protocol":"HTTP_REQUEST"
-               }
-            ],
-            "name":"sap3",
-            "functional_type":"endhost"
-         }
-      ]
-   }
+{
+    "id": 7,
+    "name": "budapest_test_case_unsat",
+    "description": "This test case verifies budapest scenario, chain sap1->webserver1 with fw blocking",
+    "policy_url_parameters": [
+        "?type=reachability&source=sap1&destination=webserver1"
+    ],
+    "results": [
+        "UNSAT"
+    ],
+    "graph": {
+        "nodes": [
+            {
+                "neighbours": [
+                    {
+                        "name": "webserver1"
+                    },
+                    {
+                        "name": "nat"
+                    }
+                ],
+                "configuration": [
+                    {
+                        "webserver1": "nat"
+                    }
+                ],
+                "name": "fw",
+                "functional_type": "firewall"
+            },
+            {
+                "neighbours": [
+                    {
+                        "name": "sap3"
+                    },
+                    {
+                        "name": "fw"
+                    }
+                ],
+                "name": "webserver1",
+                "functional_type": "webserver"
+            },
+            {
+                "neighbours": [
+                    {
+                        "name": "sap1"
+                    },
+                    {
+                        "name": "dpi"
+                    },
+                    {
+                        "name": "fw"
+                    }
+                ],
+                "configuration": [
+                    "sap1",
+                    "sap2"
+                ],
+                "name": "nat",
+                "functional_type": "nat"
+            },
+            {
+                "neighbours": [
+                    {
+                        "name": "sap2"
+                    }
+                ],
+                "configuration": [
+                    "drug"
+                ],
+                "name": "dpi",
+                "functional_type": "dpi"
+            },
+            {
+                "neighbours": [
+                    {
+                        "name": "nat"
+                    }
+                ],
+                "configuration": [
+                    {
+                        "url": "www.facebook.com",
+                        "body": "cats",
+                        "destination": "webserver1",
+                        "protocol": "HTTP_REQUEST"
+                    }
+                ],
+                "name": "sap2",
+                "functional_type": "endhost"
+            },
+            {
+                "neighbours": [
+                    {
+                        "name": "nat"
+                    }
+                ],
+                "configuration": [
+                    {
+                        "url": "www.facebook.com",
+                        "body": "cats",
+                        "destination": "webserver1",
+                        "protocol": "HTTP_REQUEST"
+                    }
+                ],
+                "name": "sap1",
+                "functional_type": "endhost"
+            },
+            {
+                "neighbours": [
+                    {
+                        "name": "webserver1"
+                    }
+                ],
+                "configuration": [
+                    {
+                        "url": "www.facebook.com",
+                        "body": "cats",
+                        "destination": "webserver1",
+                        "protocol": "HTTP_REQUEST"
+                    }
+                ],
+                "name": "sap3",
+                "functional_type": "endhost"
+            }
+        ]
+    }
 }
\ No newline at end of file
diff --git a/verigraph/tester/testcases/test_user_nat_dpi_webserver_trafficAllowed.json b/verigraph/tester/testcases/test_user_nat_dpi_webserver_trafficAllowed.json
index 8e19352..227781c 100644
--- a/verigraph/tester/testcases/test_user_nat_dpi_webserver_trafficAllowed.json
+++ b/verigraph/tester/testcases/test_user_nat_dpi_webserver_trafficAllowed.json
@@ -1,59 +1,61 @@
 {
-	"id": 2,
-	"name": "simple_test_case",
-	"description": "This test case contains a graph with client, firewall and server",
-	"policy_url_parameters": "?type=reachability&source=user1&destination=webserver",
-	"result": "SAT",
-	"graph": {
-	   "nodes":[
-	      {
-	         "name":"user1",
-	         "functional_type":"endhost",
-	         "neighbours":[
-	            {
-	               "name":"nat"
-	            }
-	         ],
-	        "configuration": 
-	            [
-					{
-						"body": "cartoon",
-						"protocol": "HTTP_REQUEST",
-						"destination": "webserver"
-					}
-	            ]
-	      },
-	      {
-	         "name":"nat",
-	         "functional_type":"nat",
-	         "neighbours":[
-	            {
-	               "name":"dpi"
-	            }
-	         ],
-	         "configuration":[
-	            "user1"
-	         ]
-	      },
-	      {
-	         "name":"dpi",
-	         "functional_type":"dpi",
-	         "neighbours":[
-	            {
-	               "name":"webserver"
-	            }
-	         ],
-	         "configuration":[
-	           "sex", "droga"
-	         ]
-	      },
-	      {
-	         "name":"webserver",
-	         "functional_type":"webserver",
-	         "neighbours":[
-	
-	         ]
-	      }
-	   ]
-	}
+    "id": 2,
+    "name": "simple_test_case",
+    "description": "This test case contains a graph with client, firewall and server",
+    "policy_url_parameters": [
+        "?type=reachability&source=user1&destination=webserver"
+    ],
+    "results": [
+        "SAT"
+    ],
+    "graph": {
+        "nodes": [
+            {
+                "name": "user1",
+                "functional_type": "endhost",
+                "neighbours": [
+                    {
+                        "name": "nat"
+                    }
+                ],
+                "configuration": [
+                    {
+                        "body": "cartoon",
+                        "protocol": "HTTP_REQUEST",
+                        "destination": "webserver"
+                    }
+                ]
+            },
+            {
+                "name": "nat",
+                "functional_type": "nat",
+                "neighbours": [
+                    {
+                        "name": "dpi"
+                    }
+                ],
+                "configuration": [
+                    "user1"
+                ]
+            },
+            {
+                "name": "dpi",
+                "functional_type": "dpi",
+                "neighbours": [
+                    {
+                        "name": "webserver"
+                    }
+                ],
+                "configuration": [
+                    "sex",
+                    "droga"
+                ]
+            },
+            {
+                "name": "webserver",
+                "functional_type": "webserver",
+                "neighbours": []
+            }
+        ]
+    }
 }
\ No newline at end of file
diff --git a/verigraph/tester/testcases/test_user_nat_dpi_webserver_trafficBlocked.json b/verigraph/tester/testcases/test_user_nat_dpi_webserver_trafficBlocked.json
index 285ecf2..6cc5b22 100644
--- a/verigraph/tester/testcases/test_user_nat_dpi_webserver_trafficBlocked.json
+++ b/verigraph/tester/testcases/test_user_nat_dpi_webserver_trafficBlocked.json
@@ -1,59 +1,61 @@
 {
-	"id": 1,
-	"name": "simple_test_case",
-	"description": "This test case contains a graph with client, firewall and server",
-	"policy_url_parameters": "?type=reachability&source=user1&destination=webserver",
-	"result": "UNSAT",
-	"graph": {
-	   "nodes":[
-	      {
-	         "name":"user1",
-	         "functional_type":"endhost",
-	         "neighbours":[
-	            {
-	               "name":"nat"
-	            }
-	         ],
-	        "configuration": 
-	            [
-					{
-						"body": "sex",
-						"protocol": "HTTP_REQUEST",
-						"destination": "webserver"
-					}
-	            ]
-	      },
-	      {
-	         "name":"nat",
-	         "functional_type":"nat",
-	         "neighbours":[
-	            {
-	               "name":"dpi"
-	            }
-	         ],
-	         "configuration":[
-	            "user1"
-	         ]
-	      },
-	      {
-	         "name":"dpi",
-	         "functional_type":"dpi",
-	         "neighbours":[
-	            {
-	               "name":"webserver"
-	            }
-	         ],
-	         "configuration":[
-	           "sex", "droga"
-	         ]
-	      },
-	      {
-	         "name":"webserver",
-	         "functional_type":"webserver",
-	         "neighbours":[
-	
-	         ]
-	      }
-	   ]
-	}
+    "id": 1,
+    "name": "simple_test_case",
+    "description": "This test case contains a graph with client, firewall and server",
+    "policy_url_parameters": [
+        "?type=reachability&source=user1&destination=webserver"
+    ],
+    "results": [
+        "UNSAT"
+    ],
+    "graph": {
+        "nodes": [
+            {
+                "name": "user1",
+                "functional_type": "endhost",
+                "neighbours": [
+                    {
+                        "name": "nat"
+                    }
+                ],
+                "configuration": [
+                    {
+                        "body": "sex",
+                        "protocol": "HTTP_REQUEST",
+                        "destination": "webserver"
+                    }
+                ]
+            },
+            {
+                "name": "nat",
+                "functional_type": "nat",
+                "neighbours": [
+                    {
+                        "name": "dpi"
+                    }
+                ],
+                "configuration": [
+                    "user1"
+                ]
+            },
+            {
+                "name": "dpi",
+                "functional_type": "dpi",
+                "neighbours": [
+                    {
+                        "name": "webserver"
+                    }
+                ],
+                "configuration": [
+                    "sex",
+                    "droga"
+                ]
+            },
+            {
+                "name": "webserver",
+                "functional_type": "webserver",
+                "neighbours": []
+            }
+        ]
+    }
 }
\ No newline at end of file
diff --git a/verigraph/tester/testcases/test_user_nat_vpn_fieldmod_webserver_unsat.json b/verigraph/tester/testcases/test_user_nat_vpn_fieldmod_webserver_unsat.json
deleted file mode 100644
index 252e3b5..0000000
--- a/verigraph/tester/testcases/test_user_nat_vpn_fieldmod_webserver_unsat.json
+++ /dev/null
@@ -1,94 +0,0 @@
-{
-	"id": 4,
-	"name": "nat_vpn_with_fieldmodifier_test_case",
-	"description": "This test case contains a graph with client, nat, vpn (with field mod in between) and server",
-	"policy_url_parameters": "?type=reachability&source=user1&destination=webserver",
-	"result": "UNSAT",
-	"graph": {
-	   "nodes":[
-	      {
-	         "name":"user1",
-	         "functional_type":"endhost",
-	         "neighbours":[
-	            {
-	               "name":"nat"
-	            }
-	         ],
-	        "configuration": 
-	            [
-					{
-						"body": "cartoon",
-						"protocol": "HTTP_REQUEST",
-						"destination": "webserver"
-					}
-	            ]
-	      },
-	      {
-	         "name":"nat",
-	         "functional_type":"nat",
-	         "neighbours":[
-	            {
-	               "name":"user1"
-	            },
-	            {
-	               "name":"vpnaccess"
-	            }
-	         ],
-	         "configuration":[
-	            "user1"
-	         ]
-	      },
-	      {
-	         "name":"vpnaccess",
-	         "functional_type":"vpnaccess",
-	         "neighbours":[
-	         	{
-	               "name":"nat"
-	            },
-	            {
-	               "name":"fieldmodifier"
-	            }
-	         ],
-	         "configuration":[
-	            {"vpnexit": "vpnexit"}
-	         ]
-	      },
-	      {
-	         "name":"fieldmodifier",
-	         "functional_type":"fieldmodifier",
-	         "neighbours":[
-	         	{
-	               "name":"vpnaccess"
-	            },
-	            {
-	               "name":"vpnexit"
-	            }
-	         ]
-	      },
-	      {
-	         "name":"vpnexit",
-	         "functional_type":"vpnexit",
-	         "neighbours":[
-	            {
-	               "name":"fieldmodifier"
-	            },
-	            {
-	               "name":"webserver"
-	            }
-	         ],
-	         "configuration":[
-	            {"vpnaccess": "vpnaccess"}
-	         ]
-	      },
-	      {
-	         "name":"webserver",
-	         "functional_type":"webserver",
-	         "neighbours":[
-	         	{
-	         		"name": "vpnexit"
-	         	}
-	         ]
-	      }
-	   ]
-	}
-}
\ No newline at end of file
diff --git a/verigraph/tester/testcases/test_user_nat_vpn_webserver_sat.json b/verigraph/tester/testcases/test_user_nat_vpn_webserver_sat.json
deleted file mode 100644
index 2ae31bc..0000000
--- a/verigraph/tester/testcases/test_user_nat_vpn_webserver_sat.json
+++ /dev/null
@@ -1,82 +0,0 @@
-{
-	"id": 3,
-	"name": "nat_vpn_test_case",
-	"description": "This test case contains a graph with client, nat, vpn and server",
-	"policy_url_parameters": "?type=reachability&source=user1&destination=webserver",
-	"result": "SAT",
-	"graph": {
-	   "nodes":[
-	      {
-	         "name":"user1",
-	         "functional_type":"endhost",
-	         "neighbours":[
-	            {
-	               "name":"nat"
-	            }
-	         ],
-	        "configuration":
-	            [
-					{
-						"body": "cartoon",
-						"protocol": "HTTP_REQUEST",
-						"destination": "webserver"
-					}
-	            ]
-	      },
-	      {
-	         "name":"nat",
-	         "functional_type":"nat",
-	         "neighbours":[
-	            {
-	               "name":"user1"
-	            },
-	            {
-	               "name":"vpnaccess"
-	            }
-	         ],
-	         "configuration":[
-	            "user1"
-	         ]
-	      },
-	      {
-	         "name":"vpnaccess",
-	         "functional_type":"vpnaccess",
-	         "neighbours":[
-	         	{
-	               "name":"nat"
-	            },
-	            {
-	               "name":"vpnexit"
-	            }
-	         ],
-	         "configuration":[
-	            {"vpnexit": "vpnexit"}
-	         ]
-	      },
-	      {
-	         "name":"vpnexit",
-	         "functional_type":"vpnexit",
-	         "neighbours":[
-	            {
-	               "name":"vpnaccess"
-	            },
-	            {
-	               "name":"webserver"
-	            }
-	         ],
-	         "configuration":[
-	            {"vpnaccess": "vpnaccess"}
-	         ]
-	      },
-	      {
-	         "name":"webserver",
-	         "functional_type":"webserver",
-	         "neighbours":[
-	         	{
-	         		"name": "vpnexit"
-	         	}
-	         ]
-	      }
-	   ]
-	}
-}
\ No newline at end of file
diff --git a/verigraph/tester/testcases/test_webserver_vpn_nat_user_unsat.json b/verigraph/tester/testcases/test_webserver_vpn_nat_user_unsat.json
deleted file mode 100644
index 60d09b3..0000000
--- a/verigraph/tester/testcases/test_webserver_vpn_nat_user_unsat.json
+++ /dev/null
@@ -1,82 +0,0 @@
-{
-	"id": 5,
-	"name": "nat_vpn_test_case_serv_to_user",
-	"description": "This test case contains a graph with client, nat, vpn and server. webserver -> client",
-	"policy_url_parameters": "?type=reachability&source=webserver&destination=user1",
-	"result": "UNSAT",
-	"graph": {
-	   "nodes":[
-	      {
-	         "name":"user1",
-	         "functional_type":"endhost",
-	         "neighbours":[
-	            {
-	               "name":"nat"
-	            }
-	         ],
-	        "configuration":
-	            [
-					{
-						"body": "cartoon",
-						"protocol": "HTTP_REQUEST",
-						"destination": "webserver"
-					}
-	            ]
-	      },
-	      {
-	         "name":"nat",
-	         "functional_type":"nat",
-	         "neighbours":[
-	            {
-	               "name":"user1"
-	            },
-	            {
-	               "name":"vpnaccess"
-	            }
-	         ],
-	         "configuration":[
-	            "user1"
-	         ]
-	      },
-	      {
-	         "name":"vpnaccess",
-	         "functional_type":"vpnaccess",
-	         "neighbours":[
-	         	{
-	               "name":"nat"
-	            },
-	            {
-	               "name":"vpnexit"
-	            }
-	         ],
-	         "configuration":[
-	            {"vpnexit": "vpnexit"}
-	         ]
-	      },
-	      {
-	         "name":"vpnexit",
-	         "functional_type":"vpnexit",
-	         "neighbours":[
-	            {
-	               "name":"vpnaccess"
-	            },
-	            {
-	               "name":"webserver"
-	            }
-	         ],
-	         "configuration":[
-	            {"vpnaccess": "vpnaccess"}
-	         ]
-	      },
-	      {
-	         "name":"webserver",
-	         "functional_type":"webserver",
-	         "neighbours":[
-	         	{
-	         		"name": "vpnexit"
-	         	}
-	         ]
-	      }
-	   ]
-	}
-}
\ No newline at end of file