verigraph/src/main/java/it/polito/escape/verify/service/VerificationService.java

   1 /*******************************************************************************
   2  * Copyright (c) 2017 Politecnico di Torino and others.
   3  *
   4  * All rights reserved. This program and the accompanying materials
   5  * are made available under the terms of the Apache License, Version 2.0
   6  * which accompanies this distribution, and is available at
   7  * http://www.apache.org/licenses/LICENSE-2.0
   8  *******************************************************************************/
   9
  10 package it.polito.escape.verify.service;
  11
  12 import java.io.BufferedReader;
  13 import java.io.File;
  14 import java.io.FileWriter;
  15 import java.io.FilenameFilter;
  16 import java.io.IOException;
  17 import java.io.InputStreamReader;
  18 import java.io.PrintWriter;
  19 import java.io.StringWriter;
  20 import java.util.ArrayList;
  21 import java.util.HashMap;
  22 import java.util.Iterator;
  23 import java.util.List;
  24 import java.util.Locale;
  25 import java.util.Map;
  26 import java.util.regex.Matcher;
  27 import java.util.regex.Pattern;
  28 import java.util.stream.Collectors;
  29
  30 import javax.tools.Diagnostic;
  31 import javax.tools.DiagnosticCollector;
  32 import javax.tools.JavaCompiler;
  33 import javax.tools.JavaFileObject;
  34 import javax.tools.StandardJavaFileManager;
  35 import javax.tools.ToolProvider;
  36 import javax.ws.rs.ProcessingException;
  37 import javax.xml.bind.JAXBException;
  38
  39 import org.json.simple.JSONArray;
  40 import org.json.simple.JSONObject;
  41
  42 import com.fasterxml.jackson.databind.JsonNode;
  43
  44 import it.polito.escape.verify.client.Neo4jManagerClient;
  45 import it.polito.escape.verify.exception.BadRequestException;
  46 import it.polito.escape.verify.exception.DataNotFoundException;
  47 import it.polito.escape.verify.exception.ForbiddenException;
  48 import it.polito.escape.verify.exception.InternalServerErrorException;
  49 import it.polito.escape.verify.model.Configuration;
  50 import it.polito.escape.verify.model.Entry;
  51 import it.polito.escape.verify.model.Graph;
  52 import it.polito.escape.verify.model.Neighbour;
  53 import it.polito.escape.verify.model.Node;
  54 import it.polito.escape.verify.model.Test;
  55 import it.polito.escape.verify.model.Verification;
  56 import it.polito.escape.verify.resources.beans.VerificationBean;
  57 import it.polito.nffg.neo4j.jaxb.Paths;
  58 import qj.util.ReflectUtil;
  59 import qj.util.lang.DynamicClassLoader;
  60
  61 public class VerificationService {
  62
  63         private static final String     generatorFolder         = System.getProperty("catalina.base")
  64                                                                                                                 + "/webapps/verify/WEB-INF/classes/tests/j-verigraph-generator";
  65
  66         private static final String     generatorFolderForGrpc  = "service/src/tests/j-verigraph-generator";
  67
  68         private String                          testClassGenerator      = generatorFolder + "/test_class_generator.py";
  69
  70         private String                          testGenerator           = generatorFolder + "/test_generator.py";
  71
  72         public VerificationService() {
  73
  74         }
  75
  76         private Paths getPaths(Graph graph, Node sourceNode, Node destinationNode) {
  77
  78                 String source = sourceNode.getName() + "_" + sourceNode.getId();
  79                 String destination = destinationNode.getName() + "_" + destinationNode.getId();
  80
  81                 List<String> endpoints = new ArrayList<>();
  82                 List<String> firewalls = new ArrayList<>();
  83                 Map<String, List<Entry>> routingTable = new HashMap<>();
  84
  85                 for (Node node : graph.getNodes().values()) {
  86                         // if firewall
  87                         if (node.getFunctional_type().equals("NF")) {
  88                                 // add 2 connection points to RT
  89                                 routingTable.put(node.getName() + "_" + node.getId() + "_in", new ArrayList<Entry>());
  90                                 routingTable.put(node.getName() + "_" + node.getId() + "_out", new ArrayList<Entry>());
  91                                 // add node to firewalls
  92                                 firewalls.add(node.getName() + "_" + node.getId());
  93                                 // scan neighbours
  94                                 for (Neighbour neighbour : node.getNeighbours().values()) {
  95                                         // check if neighbour is a firewall
  96                                         Node hop = graph.searchNodeByName(neighbour.getName());
  97                                         // if neighbour is a firewall connect to its input port
  98                                         if (hop.getFunctional_type().equals("NF"))
  99                                                 routingTable.get(node.getName() + "_" + node.getId() + "_out")
 100                                                                         .add(new Entry("output", neighbour.getName() + "_" + hop.getId() + "_in"));
 101                                         else
 102                                                                                                                                 // connect
 103                                                                                                                                 // normally to
 104                                                                                                                                 // node
 105                                                                                                                                 routingTable.get(node.getName() + "_" + node.getId()
 106                                                                                                                                                                         + "_out")
 107                                                                                                                                                         .add(new Entry( "output",
 108                                                                                                                                                                                         neighbour.getName()     + "_"
 109                                                                                                                                                                                                                 + hop.getId()));
 110                                 }
 111                         }
 112                         // if endpoint
 113                         else {
 114                                 // add endpoint to RT
 115                                 routingTable.put(node.getName() + "_" + node.getId(), new ArrayList<Entry>());
 116                                 // add to endpoints
 117                                 endpoints.add(node.getName() + "_" + node.getId());
 118                                 // scan neighbours
 119                                 for (Neighbour neighbour : node.getNeighbours().values()) {
 120                                         // check if neighbour is a firewall
 121                                         Node hop = graph.searchNodeByName(neighbour.getName());
 122                                         // if neighbour is a firewall connect to its input port
 123                                         if (hop.getFunctional_type().equals("NF"))
 124                                                 routingTable.get(node.getName() + "_" + node.getId())
 125                                                                         .add(new Entry("output", neighbour.getName() + "_" + hop.getId() + "_in"));
 126                                         else {
 127                                                 // connect
 128                                                 // normally to
 129                                                 // node
 130                                                 routingTable.get(node.getName() + "_" + node.getId())
 131                                                                         .add(new Entry("output", neighbour.getName() + "_" + hop.getId()));
 132                                         }
 133                                 }
 134                         }
 135
 136                         // end node scan
 137                 }
 138                 // debug print
 139                 System.out.println("Endpoints:");
 140                 for (String endpoint : endpoints) {
 141                         System.out.println(endpoint);
 142                 }
 143                 System.out.println("Firewalls:");
 144                 for (String firewall : firewalls) {
 145                         System.out.println(firewall);
 146                 }
 147                 System.out.println("Source: " + source);
 148                 System.out.println("Destination: " + destination);
 149                 for (String key : routingTable.keySet()) {
 150                         System.out.println("RT for node " + key);
 151                         for (Entry entry : routingTable.get(key)) {
 152                                 System.out.println("\t" + entry.getDirection() + "->" + entry.getDestination());
 153                         }
 154                 }
 155                 // end debug print
 156
 157                 Neo4jManagerClient client = new Neo4jManagerClient(     "http://localhost:8080/neo4jmanager/rest/",
 158                                                                                                                         source,
 159                                                                                                                         destination,
 160                                                                                                                         endpoints,
 161                                                                                                                         firewalls,
 162                                                                                                                         routingTable);
 163
 164                 Paths paths = null;
 165                 try {
 166                         paths = client.getPaths();
 167                 }
 168                 catch (JAXBException e) {
 169                         throw new InternalServerErrorException("Error generating input for neo4jmanager: " + e.getMessage());
 170                 }
 171                 catch (ProcessingException e) {
 172                         throw new InternalServerErrorException("Response of neo4jmanager doesn't contain any path: "
 173                                                                                                         + e.getMessage());
 174                 }
 175                 catch (IllegalStateException e) {
 176                         throw new InternalServerErrorException("Error getting a response from neo4jmanager, no input stream for paths or input stream already consumed: "
 177                                                                                                         + e.getMessage());
 178                 }
 179                 catch (Exception e) {
 180                         throw new InternalServerErrorException("Unable to continue due to a neo4jmanager error: " + e.getMessage());
 181                 }
 182
 183                 return paths;
 184
 185         }
 186
 187         private List<String> sanitizePath(String path) {
 188                 List<String> newPath = new ArrayList<String>();
 189                 // find all nodes, i.e. all names between parentheses
 190                 Matcher m = Pattern.compile("\\(([^)]+)\\)").matcher(path);
 191                 while (m.find()) {
 192                         String node = m.group(1);
 193
 194                         int spaceIndex = node.lastIndexOf("_");
 195                         if (spaceIndex != -1) {
 196                                 node = node.substring(0, spaceIndex);
 197                                 newPath.add(node);
 198                         }
 199                 }
 200                 return newPath;
 201
 202         }
 203
 204         private List<List<String>> sanitizePaths(Paths paths) {
 205                 List<List<String>> sanitizedPaths = new ArrayList<List<String>>();
 206                 for (String path : paths.getPath()) {
 207                         System.out.println("Original path: " + path);
 208                         List<String> newPath = sanitizePath(path);
 209                         sanitizedPaths.add(newPath);
 210                 }
 211                 return sanitizedPaths;
 212         }
 213
 214         static private Map<String, Long> toMap(List<String> lst) {
 215                 return lst.stream().collect(Collectors.groupingBy(s -> s, Collectors.counting()));
 216         }
 217
 218         private void eliminateLoopsInPaths(List<List<String>> sanitizedPaths) {
 219                 List<List<String>> pathsToBeRemoved = new ArrayList<List<String>>();
 220
 221                 for (List<String> path : sanitizedPaths) {
 222                         Map<String, Long> occurrencesMap = toMap(path);
 223                         for (long occurrences : occurrencesMap.values()) {
 224                                 if (occurrences > 1) {
 225                                         pathsToBeRemoved.add(path);
 226                                         break;
 227                                 }
 228                         }
 229                 }
 230                 for (List<String> path : pathsToBeRemoved) {
 231                         sanitizedPaths.remove(path);
 232                 }
 233         }
 234
 235         private void printListsOfStrings(String message, List<List<String>> lists) {
 236                 System.out.println(message);
 237                 for (List<String> element : lists) {
 238                         System.out.println(element);
 239                 }
 240         }
 241
 242         private static File createTempDir(String prefix) throws IOException {
 243                 String tmpDirStr = System.getProperty("java.io.tmpdir");
 244                 if (tmpDirStr == null) {
 245                         throw new IOException("System property 'java.io.tmpdir' does not specify a tmp dir");
 246                 }
 247
 248                 File tmpDir = new File(tmpDirStr);
 249                 if (!tmpDir.exists()) {
 250                         boolean created = tmpDir.mkdirs();
 251                         if (!created) {
 252                                 throw new IOException("Unable to create tmp dir " + tmpDir);
 253                         }
 254                 }
 255
 256                 File resultDir = null;
 257                 int suffix = (int) System.currentTimeMillis();
 258                 int failureCount = 0;
 259                 do {
 260                         resultDir = new File(tmpDir, prefix + suffix % 10000);
 261                         suffix++;
 262                         failureCount++;
 263                 } while (resultDir.exists() && failureCount < 50);
 264
 265                 if (resultDir.exists()) {
 266                         throw new IOException(failureCount
 267                                                                         + " attempts to generate a non-existent directory name failed, giving up");
 268                 }
 269                 boolean created = resultDir.mkdir();
 270                 if (!created) {
 271                         throw new IOException("Failed to create tmp directory");
 272                 }
 273
 274                 return resultDir;
 275         }
 276
 277         @SuppressWarnings("unchecked")
 278         private void generateChainsFile(Graph graph, List<List<String>> sanitizedPaths, String chainsFile) {
 279                 JSONObject root = new JSONObject();
 280                 JSONArray chains = new JSONArray();
 281
 282                 int chainCounter = 0;
 283
 284                 for (List<String> path : sanitizedPaths) {
 285                         Iterator<String> pathsIterator = path.iterator();
 286                         JSONObject chain = new JSONObject();
 287                         chain.put("id", ++chainCounter);
 288                         chain.put("flowspace", "tcp=80");
 289                         JSONArray nodes = new JSONArray();
 290                         while (pathsIterator.hasNext()) {
 291                                 String nodeName = (String) pathsIterator.next();
 292                                 Node currentNode = graph.searchNodeByName(nodeName);
 293                                 if (currentNode == null) {
 294                                         throw new InternalServerErrorException("Unable to generate 'chains.json' for neo4jmanager: node "
 295                                                                                                                         + nodeName + " not found");
 296                                 }
 297                                 JSONObject node = new JSONObject();
 298                                 node.put("name", currentNode.getName());
 299                                 // if(currentNode.getFunctional_type().equals("firewall"))
 300                                 // node.put("address", "ip_nat");
 301                                 // else
 302                                 node.put("address", "ip_" + currentNode.getName());
 303                                 node.put("functional_type", currentNode.getFunctional_type());
 304                                 nodes.add(node);
 305                                 chain.put("nodes", nodes);
 306                         }
 307                         chains.add(chain);
 308                 }
 309                 root.put("chains", chains);
 310
 311                 try (FileWriter file = new FileWriter(chainsFile)) {
 312                         file.write(root.toJSONString());
 313                         System.out.println("Successfully created 'chains.json' with the following content:");
 314                         System.out.println(root);
 315                 }
 316                 catch (IOException e) {
 317                         throw new InternalServerErrorException("Error saving 'chains.json' for neo4jmanager");
 318                 }
 319
 320         }
 321
 322         @SuppressWarnings("unchecked")
 323         private void generateConfigFile(Graph graph, String configFile) {
 324                 JSONObject root = new JSONObject();
 325                 JSONArray nodes = new JSONArray();
 326
 327                 for (Node n : graph.getNodes().values()) {
 328                         JSONObject node = new JSONObject();
 329                         // JSONArray configuration = new JSONArray();
 330                         Configuration nodeConfig = n.getConfiguration();
 331                         JsonNode configuration = nodeConfig.getConfiguration();
 332
 333                         node.put("configuration", configuration);
 334                         node.put("id", nodeConfig.getId());
 335                         node.put("description", nodeConfig.getDescription());
 336
 337                         nodes.add(node);
 338
 339                 }
 340                 root.put("nodes", nodes);
 341
 342                 try (FileWriter file = new FileWriter(configFile)) {
 343                         file.write(root.toJSONString());
 344                         System.out.println("Successfully created 'config.json' with the following content:");
 345                         System.out.println(root);
 346                 }
 347                 catch (IOException e) {
 348                         throw new InternalServerErrorException("Error saving 'config.json' for neo4jmanager");
 349                 }
 350
 351         }
 352
 353         private void printCommand(String[] cmd) {
 354                 for (String c : cmd) {
 355                         System.out.printf(c + " ");
 356                 }
 357                 System.out.println("");
 358         }
 359
 360         private String platfromIndependentPath(String path) {
 361                 path = path.replaceAll("/", Matcher.quoteReplacement(Character.toString(File.separatorChar)));
 362                 return path;
 363         }
 364
 365         private void generateTestScenarios(String chainsFile, String configFile, String scenarioFile) {
 366
 367                 String[] cmd = {        "python", platfromIndependentPath(testClassGenerator), "-c",
 368                                                         platfromIndependentPath(chainsFile), "-f", platfromIndependentPath(configFile), "-o",
 369                                                         platfromIndependentPath(scenarioFile) };
 370                 printCommand(cmd);
 371
 372                 ProcessBuilder pb = new ProcessBuilder(cmd);
 373                 pb.redirectErrorStream(true);
 374                 Process process;
 375                 try {
 376                         process = pb.start();
 377
 378                         BufferedReader reader = new BufferedReader(new InputStreamReader(process.getInputStream()));
 379                         String line;
 380                         while ((line = reader.readLine()) != null)
 381                                 System.out.println("test_class_generator.py: " + line);
 382                         process.waitFor();
 383                         if (process.exitValue() != 0) {
 384                                 throw new InternalServerErrorException("Unable to generate test scenario file for the verification request: test_class_generator returned "
 385                                                                                                                 + process.exitValue());
 386                         }
 387                 }
 388                 catch (IOException e) {
 389                         throw new InternalServerErrorException("Error generating tests for Z3: unable to execute generator");
 390                 }
 391                 catch (InterruptedException e) {
 392                         throw new InternalServerErrorException("Error generating tests for Z3: generator got interrupted during execution");
 393                 }
 394
 395         }
 396
 397         private void generateTests(     int scenariosCounter, String scenariosBasename, String source, String destination,
 398                                                                 String testsBasename) {
 399
 400                 List<String> scenarios = new ArrayList<String>();
 401                 List<String> tests = new ArrayList<String>();
 402                 for (int i = 0; i < scenariosCounter; i++) {
 403                         scenarios.add(scenariosBasename + "_" + (i + 1) + ".java");
 404                         tests.add(testsBasename + "_" + (i + 1) + ".java");
 405                 }
 406
 407                 for (int i = 0; i < scenariosCounter; i++) {
 408                         String[] cmd = {        "python", platfromIndependentPath(testGenerator), "-i",
 409                                                                 platfromIndependentPath(scenarios.get(i)), "-o", platfromIndependentPath(tests.get(i)),
 410                                                                 "-s", source, "-d", destination };
 411                         printCommand(cmd);
 412
 413                         ProcessBuilder pb = new ProcessBuilder(cmd);
 414                         pb.redirectErrorStream(true);
 415                         Process process;
 416                         try {
 417                                 process = pb.start();
 418
 419                                 BufferedReader reader = new BufferedReader(new InputStreamReader(process.getInputStream()));
 420                                 String line;
 421                                 while ((line = reader.readLine()) != null)
 422                                         System.out.println("test_generator.py: " + line);
 423                                 process.waitFor();
 424                                 if (process.exitValue() != 0) {
 425                                         throw new InternalServerErrorException("Unable to generate test file for the verification request: test_generator returned "
 426                                                                                                                         + process.exitValue());
 427                                 }
 428                         }
 429                         catch (IOException e) {
 430                                 throw new InternalServerErrorException("Error generating tests for Z3: unable to execute generator");
 431                         }
 432                         catch (InterruptedException e) {
 433                                 throw new InternalServerErrorException("Error generating tests for Z3: generator got interrupted during execution");
 434                         }
 435
 436                 }
 437
 438         }
 439
 440         private void prepareForCompilationAndExecution( int scenariosCounter, String scenarioBasename, String testBasename,
 441                                                                                                         List<File> sourceFiles, List<File> classFiles) {
 442                 for (int i = 0; i < scenariosCounter; i++) {
 443                         String scenario = scenarioBasename + "_" + (i + 1) + ".java";
 444                         sourceFiles.add(new File(scenario));
 445                         System.out.println("Scenario file " + scenario + " added to compilation");
 446
 447                         String testSource = testBasename + "_" + (i + 1) + ".java";
 448                         String testClass = testBasename + "_" + (i + 1);
 449
 450                         sourceFiles.add(new File(testSource));
 451                         System.out.println("Test file " + testSource + " added to copilation");
 452                         classFiles.add(new File(testClass));
 453                         System.out.println("Test file " + testClass + " added to execution");
 454                 }
 455         }
 456
 457         private void compileFiles(List<File> files, String folder) {
 458
 459                 JavaCompiler compiler = ToolProvider.getSystemJavaCompiler();
 460                 if (compiler == null) {
 461                         throw new InternalServerErrorException("Error getting the Java compiler: JDK >= 1.8 required");
 462                 }
 463                 StandardJavaFileManager fileManager = compiler.getStandardFileManager(null, null, null);
 464
 465                 try {
 466                         // fileManager.setLocation(StandardLocation.CLASS_OUTPUT,
 467                         // Arrays.asList(new File(projectFolder)));
 468
 469                         // String z3 = "/usr/lib/com.microsoft.z3.jar";
 470                         // List<String> optionList = new ArrayList<String>();
 471                         // optionList.add("-classpath");
 472                         // optionList.add(System.getProperty("java.class.path") + ":" + z3);
 473                         List<String> optionList = new ArrayList<String>();
 474                         optionList.add("-d");
 475                         optionList.add(folder);
 476                         DiagnosticCollector<JavaFileObject> diagnostics = new DiagnosticCollector<>();
 477
 478                         boolean success = compiler
 479                                                                                 .getTask(       null,
 480                                                                                                         fileManager,
 481                                                                                                         diagnostics,
 482                                                                                                         optionList,
 483                                                                                                         null,
 484                                                                                                         fileManager.getJavaFileObjectsFromFiles(files))
 485                                                                                 .call();
 486                         if (!success) {
 487                                 Locale myLocale = Locale.getDefault();
 488                                 StringBuilder msg = new StringBuilder();
 489                                 msg.append("Error compiling Z3 test files: ");
 490                                 for (Diagnostic<? extends JavaFileObject> err : diagnostics.getDiagnostics()) {
 491                                         msg.append('\n');
 492                                         msg.append(err.getKind());
 493                                         msg.append(": ");
 494                                         if (err.getSource() != null) {
 495                                                 msg.append(err.getSource().getName());
 496                                         }
 497                                         msg.append(':');
 498                                         msg.append(err.getLineNumber());
 499                                         msg.append(": ");
 500                                         msg.append(err.getMessage(myLocale));
 501                                 }
 502                                 throw new InternalServerErrorException(msg.toString());
 503                         }
 504                         fileManager.close();
 505
 506                 }
 507                 catch (IOException e) {
 508                         throw new InternalServerErrorException("Unable to set the location of the Z3 test files to be compiled");
 509                 }
 510
 511         }
 512
 513         private int runIt(File filename, String folder) {
 514                 int endIndex = filename.getName().lastIndexOf(".");
 515                 String filenameNoExtension;
 516                 if (endIndex == -1) {
 517                         filenameNoExtension = filename.getName();
 518                 }
 519                 else {
 520                         filenameNoExtension = filename.getName().substring(0, endIndex);
 521                         if (!filenameNoExtension.matches("\\w+")) {
 522                                 filenameNoExtension = filename.getName();
 523                         }
 524                 }
 525
 526                 System.out.println("Filename is: " + filenameNoExtension);
 527                 try {
 528                         Class<?> userClass = new DynamicClassLoader(folder).load("tests." + filenameNoExtension);
 529                         Object context = ReflectUtil.newInstance(userClass);
 530                         Object result = ReflectUtil.invoke("run", context);
 531                         return (int) result;
 532                 }
 533                 catch (Exception e) {
 534                         StringWriter errors = new StringWriter();
 535                         e.printStackTrace(new PrintWriter(errors));
 536                         throw new InternalServerErrorException("Error executing Z3 tests: "     + e.getMessage()
 537                                                                                                         + ". There are errors in the Z3 model.");
 538                 }
 539         }
 540
 541         private List<Test> runFiles(String folder, List<List<String>> paths, Graph graph, List<File> files) {
 542                 List<Test> tests = new ArrayList<Test>();
 543                 for (int i = 0; i < files.size(); i++) {
 544                         System.out.println("Running test file \"" + files.get(i).getAbsolutePath() + "\"");
 545                         int result = runIt(files.get(i), folder);
 546                         System.out.println("Execution returned: " + result);
 547
 548                         List<Node> path = new ArrayList<Node>();
 549                         for (String nodeString : paths.get(i)) {
 550                                 Node node = graph.searchNodeByName(nodeString);
 551                                 path.add(node);
 552                         }
 553                         Test t = new Test(path, result);
 554                         tests.add(t);
 555                 }
 556
 557                 return tests;
 558         }
 559
 560         @SuppressWarnings("unused")
 561         private static boolean deleteDir(File dir) {
 562                 if (dir.isDirectory()) {
 563                         String[] children = dir.list();
 564                         for (int i = 0; i < children.length; i++) {
 565                                 boolean success = deleteDir(new File(dir, children[i]));
 566                                 if (!success) {
 567                                         return false;
 568                                 }
 569                         }
 570                 }
 571
 572                 return dir.delete();
 573
 574         }
 575
 576         @SuppressWarnings("unused")
 577         private void deleteFilesWithPrefix(String directory, String prefix, String extension) {
 578                 final File scenarioFolder = new File(directory);
 579                 final File[] scenarioFiles = scenarioFolder.listFiles(new FilenameFilter() {
 580
 581                         @Override
 582                         public boolean accept(final File dir, final String name) {
 583                                 return name.matches(prefix + ".*\\." + extension);
 584                         }
 585                 });
 586                 for (final File file : scenarioFiles) {
 587                         if (!file.delete()) {
 588                                 System.err.println("Can't remove " + file.getAbsolutePath());
 589                         }
 590                         else {
 591                                 System.out.println("Removed file " + file.getAbsolutePath());
 592                         }
 593                 }
 594         }
 595
 596         public Verification verify(long graphId, VerificationBean verificationBean) {
 597                 if (graphId <= 0) {
 598                         throw new ForbiddenException("Illegal graph id: " + graphId);
 599                 }
 600                 GraphService graphService = new GraphService();
 601                 Graph graph = graphService.getGraph(graphId);
 602                 if (graph == null) {
 603                         throw new DataNotFoundException("Graph with id " + graphId + " not found");
 604                 }
 605                 String source = verificationBean.getSource();
 606                 String destination = verificationBean.getDestination();
 607                 String type = verificationBean.getType();
 608                 if (source == null || source.equals("")) {
 609                         throw new BadRequestException("Please specify the 'source' parameter in your request");
 610                 }
 611                 if (destination == null || destination.equals("")) {
 612                         throw new BadRequestException("Please specify the 'destination' parameter in your request");
 613                 }
 614                 if (type == null || type.equals("")) {
 615                         throw new BadRequestException("Please specify the 'type' parameter in your request");
 616                 }
 617
 618                 Node sourceNode = graph.searchNodeByName(verificationBean.getSource());
 619                 Node destinationNode = graph.searchNodeByName(verificationBean.getDestination());
 620
 621                 if (sourceNode == null) {
 622                         throw new BadRequestException("The 'source' parameter '" + source + "' is not valid, please insert the name of an existing node");
 623                 }
 624                 if (destinationNode == null) {
 625                         throw new BadRequestException("The 'destination' parameter '" + destination + "' is not valid, please insert the name of an existing node");
 626                 }
 627                 if ((!type.equals("reachability")) && (!type.equals("isolation")) && (!type.equals("traversal"))) {
 628                         throw new BadRequestException("The 'type' parameter '"  + type
 629                                                                                         + "' is not valid: valid types are: 'reachability', 'isolation' and 'traversal'");
 630                 }
 631
 632                 Verification v = null;
 633                 String middlebox;
 634                 Node middleboxNode;
 635                 switch (type) {
 636                         case "reachability":
 637                                 v = reachabilityVerification(graph, sourceNode, destinationNode);
 638                                 break;
 639                         case "isolation":
 640                                 middlebox = verificationBean.getMiddlebox();
 641                                 if (middlebox == null || middlebox.equals("")) {
 642                                         throw new BadRequestException("Please specify the 'middlebox' parameter in your request");
 643                                 }
 644
 645                                 middleboxNode = graph.searchNodeByName(middlebox);
 646                                 if (middleboxNode == null) {
 647                                         throw new BadRequestException("The 'middlebox' parameter '" + middlebox + "' is not valid, please insert the name of an existing node");
 648                                 }
 649                                 if (middleboxNode.getFunctional_type().equals("endpoint")) {
 650                                         throw new BadRequestException("'"       + middlebox
 651                                                                                                         + "' is of type 'endpoint', please choose a valid middlebox");
 652                                 }
 653                                 v = isolationVerification(graph, sourceNode, destinationNode, middleboxNode);
 654                                 break;
 655                         case "traversal":
 656                                 middlebox = verificationBean.getMiddlebox();
 657                                 if (middlebox == null || middlebox.equals("")) {
 658                                         throw new BadRequestException("Please specify the 'middlebox' parameter in your request");
 659                                 }
 660
 661                                 middleboxNode = graph.searchNodeByName(middlebox);
 662                                 if (middleboxNode == null) {
 663                                         throw new BadRequestException("The 'middlebox' parameter '" + middlebox + "' is not valid, please insert the name of an existing node");
 664                                 }
 665                                 if (middleboxNode.getFunctional_type().equals("endpoint")) {
 666                                         throw new BadRequestException("'"       + middlebox
 667                                                                                                         + "' is of type 'endpoint', please choose a valid middlebox");
 668                                 }
 669                                 v = traversalVerification(graph, sourceNode, destinationNode, middleboxNode);
 670                                 break;
 671                         default:
 672                                 break;
 673                 }
 674
 675                 return v;
 676         }
 677
 678         private Verification isolationVerification(Graph graph, Node sourceNode, Node destinationNode, Node middleboxNode) {
 679
 680                 Paths paths = getPaths(graph, sourceNode, destinationNode);
 681                 if (paths.getPath().size() == 0) {
 682                         return new Verification("UNSAT",
 683                                                                         "There are no available paths between '"        + sourceNode.getName() + "' and '"
 684                                                                                                 + destinationNode.getName() + "'");
 685                 }
 686
 687                 List<List<String>> sanitizedPaths = sanitizePaths(paths);
 688
 689                 printListsOfStrings("Before loops removal", sanitizedPaths);
 690
 691                 eliminateLoopsInPaths(sanitizedPaths);
 692
 693                 printListsOfStrings("After loops removal", sanitizedPaths);
 694
 695                 if (sanitizedPaths.isEmpty()) {
 696                         return new Verification("UNSAT",
 697                                                                         "There are no available paths between '"        + sourceNode.getName() + "' and '"
 698                                                                                                 + destinationNode.getName() + "'");
 699                 }
 700
 701                 List<Test> tests = extractTestsFromPaths(graph, sanitizedPaths, "UNKNWON");
 702
 703                 extractPathsWithMiddlebox(sanitizedPaths, middleboxNode.getName());
 704
 705                 if (sanitizedPaths.isEmpty()) {
 706                         return new Verification("UNSAT",
 707                                                                         tests,
 708                                                                         "There are no available paths between '"        + sourceNode.getName() + "' and '"
 709                                                                                         + destinationNode.getName() + "' which traverse middlebox '"
 710                                                                                         + middleboxNode.getName() + "'. See below all the available paths.");
 711                 }
 712
 713                 printListsOfStrings("Paths with middlebox '" + middleboxNode.getName() + "'", sanitizedPaths);
 714
 715                 File tempDir = null;
 716
 717                 try {
 718                         tempDir = createTempDir("isolation");
 719                 }
 720                 catch (IOException e) {
 721                         throw new InternalServerErrorException("Unable to perform verification: " + e.getMessage());
 722                 }
 723
 724                 String chainsFile = tempDir.getAbsolutePath() + "/chains.json";
 725                 generateChainsFile(graph, sanitizedPaths, chainsFile);
 726
 727                 String configFile = tempDir.getAbsolutePath() + "/config.json";
 728                 generateConfigFile(graph, configFile);
 729
 730                 String isolationScenariosBasename = tempDir.getAbsolutePath() + "/IsolationScenario";
 731                 try{
 732                         generateTestScenarios(chainsFile, configFile, isolationScenariosBasename);
 733                 }catch(Exception ex){
 734                         testClassGenerator = generatorFolderForGrpc + "/test_class_generator.py";
 735                         generateTestScenarios(chainsFile, configFile, isolationScenariosBasename);
 736                 }
 737
 738                 String isolationTestsBasename = tempDir.getAbsolutePath() + "/IsolationTest";
 739                 try{
 740                         generateTests(  sanitizedPaths.size(),
 741                                         isolationScenariosBasename,
 742                                         sourceNode.getName(),
 743                                         middleboxNode.getName(),
 744                                         isolationTestsBasename);
 745                 }catch(InternalServerErrorException ex){
 746                         testGenerator = generatorFolderForGrpc + "/test_generator.py";
 747                         generateTests(  sanitizedPaths.size(),
 748                                         isolationScenariosBasename,
 749                                         sourceNode.getName(),
 750                                         middleboxNode.getName(),
 751                                         isolationTestsBasename);
 752                 }
 753
 754                 List<File> sourceFiles = new ArrayList<File>();
 755                 List<File> classFiles = new ArrayList<File>();
 756                 prepareForCompilationAndExecution(      sanitizedPaths.size(),
 757                                 isolationScenariosBasename,
 758                                                                                         isolationTestsBasename,
 759                                                                                         sourceFiles,
 760                                                                                         classFiles);
 761
 762                 compileFiles(sourceFiles, tempDir.getAbsolutePath());
 763
 764                 tests = runFiles(tempDir.getAbsolutePath(), sanitizedPaths, graph, classFiles);
 765
 766                 return evaluateIsolationResults(tests,
 767                                                                                 sourceNode.getName(),
 768                                                                                 destinationNode.getName(),
 769                                                                                 middleboxNode.getName());
 770
 771         }
 772
 773         private List<Test> extractTestsFromPaths(Graph graph, List<List<String>> paths, String result) {
 774                 List<Test> tests = new ArrayList<Test>();
 775                 for (List<String> path : paths) {
 776                         List<Node> nodes = new ArrayList<Node>();
 777                         for (String nodeName : path) {
 778                                 nodes.add(graph.searchNodeByName(nodeName));
 779                         }
 780                         tests.add(new Test(nodes, result));
 781                 }
 782                 return tests;
 783         }
 784
 785         private Verification evaluateIsolationResults(  List<Test> tests, String source, String destination,
 786                                                                                                         String middlebox) {
 787                 Verification v = new Verification();
 788                 boolean isSat = false;
 789                 int unsatCounter = 0;
 790                 for (Test t : tests) {
 791                         v.getTests().add(t);
 792
 793                         if (t.getResult().equals("SAT")) {
 794                                 isSat = true;
 795                         }
 796                         else if (t.getResult().equals("UNKNOWN")) {
 797                                 v.setResult("UNKNWON");
 798                                 v.setComment("Isolation property with source '" + source + "', destination '" + destination
 799                                                                 + "' and middlebox '" + middlebox + "' is UNKNOWN because although '" + source
 800                                                                 + "' cannot reach '" + middlebox + "' in any path from '" + source + "' to '"
 801                                                                 + destination + "' which traverses middlebox '" + middlebox
 802                                                                 + "' at least one reachability test between '" + source + "' and '" + middlebox
 803                                                                 + "' returned UNKNOWN (see below all the paths that have been checked)");
 804                         }
 805                         else if (t.getResult().equals("UNSAT")) {
 806                                 unsatCounter++;
 807                         }
 808                 }
 809                 if (isSat) {
 810                         v.setResult("UNSAT");
 811                         v.setComment("Isolation property with source '" + source + "', destination '" + destination
 812                                                         + "' and middlebox '" + middlebox + "' is UNSATISFIED because reachability between '"
 813                                                         + source + "' and '" + middlebox + "' is SATISFIED in at least one path between '" + source
 814                                                         + "' and '" + destination + "' which traverses middlebox '" + middlebox
 815                                                         + "' (see below all the paths that have been checked)");
 816                 }
 817                 else if (unsatCounter == tests.size()) {
 818                         v.setResult("SAT");
 819                         v.setComment("Isolation property with source '" + source + "', destination '" + destination
 820                                                         + "' and middlebox '" + middlebox + "' is SATISFIED because reachability between '" + source
 821                                                         + "' and '" + middlebox + "' is UNSATISFIED in all paths between '" + source + "' and '"
 822                                                         + destination + "' which traverse middlebox '" + middlebox
 823                                                         + "' (see below all the paths that have been checked)");
 824                 }
 825                 return v;
 826
 827         }
 828
 829         private void extractPathsWithMiddlebox(List<List<String>> sanitizedPaths, String middleboxName) {
 830                 List<List<String>> pathsToBeRemoved = new ArrayList<List<String>>();
 831                 for (List<String> path : sanitizedPaths) {
 832                         boolean middleboxFound = false;
 833                         for (String node : path) {
 834                                 if (node.equals(middleboxName)) {
 835                                         middleboxFound = true;
 836                                         break;
 837                                 }
 838                         }
 839                         if (!middleboxFound) {
 840                                 pathsToBeRemoved.add(path);
 841                         }
 842                 }
 843
 844                 for (List<String> path : pathsToBeRemoved) {
 845                         sanitizedPaths.remove(path);
 846                 }
 847
 848         }
 849
 850         private void extractPathsWithoutMiddlebox(List<List<String>> sanitizedPaths, String middleboxName) {
 851                 List<List<String>> pathsToBeRemoved = new ArrayList<List<String>>();
 852                 for (List<String> path : sanitizedPaths) {
 853                         boolean middleboxFound = false;
 854                         for (String node : path) {
 855                                 if (node.equals(middleboxName)) {
 856                                         middleboxFound = true;
 857                                         break;
 858                                 }
 859                         }
 860                         if (middleboxFound) {
 861                                 pathsToBeRemoved.add(path);
 862                         }
 863                 }
 864
 865                 for (List<String> path : pathsToBeRemoved) {
 866                         sanitizedPaths.remove(path);
 867                 }
 868
 869         }
 870
 871         private Verification traversalVerification(Graph graph, Node sourceNode, Node destinationNode, Node middleboxNode) {
 872
 873                 Paths paths = getPaths(graph, sourceNode, destinationNode);
 874                 if (paths.getPath().size() == 0) {
 875                         return new Verification("UNSAT",
 876                                                                         "There are no available paths between '"        + sourceNode.getName() + "' and '"
 877                                                                                                 + destinationNode.getName() + "'");
 878                 }
 879
 880                 List<List<String>> pathsBetweenSourceAndDestination = sanitizePaths(paths);
 881
 882                 printListsOfStrings("Before loops removal", pathsBetweenSourceAndDestination);
 883
 884                 eliminateLoopsInPaths(pathsBetweenSourceAndDestination);
 885
 886                 printListsOfStrings("After loops removal", pathsBetweenSourceAndDestination);
 887
 888                 if (pathsBetweenSourceAndDestination.isEmpty()) {
 889                         return new Verification("UNSAT",
 890                                                                         "There are no available paths between '"        + sourceNode.getName() + "' and '"
 891                                                                                                 + destinationNode.getName() + "'");
 892                 }
 893
 894                 List<Test> tests = extractTestsFromPaths(graph, pathsBetweenSourceAndDestination, "UNKNOWN");
 895
 896                 List<List<String>> pathsWithMiddlebox = new ArrayList<List<String>>();
 897                 for (List<String> path : pathsBetweenSourceAndDestination) {
 898                         pathsWithMiddlebox.add(path);
 899                 }
 900
 901                 extractPathsWithMiddlebox(pathsWithMiddlebox, middleboxNode.getName());
 902
 903                 if (pathsWithMiddlebox.isEmpty()) {
 904                         return new Verification("UNSAT",
 905                                                                         tests,
 906                                                                         "There are no paths between '"  + sourceNode.getName() + "' and '"
 907                                                                                         + destinationNode.getName() + "' which traverse middlebox '"
 908                                                                                         + middleboxNode.getName() + "'. See below all the available paths");
 909                 }
 910
 911                 printListsOfStrings("Paths with middlebox '" + middleboxNode.getName() + "'", pathsWithMiddlebox);
 912
 913                 File tempDir = null;
 914
 915                 try {
 916                         tempDir = createTempDir("traversal");
 917                 }
 918                 catch (IOException e) {
 919                         throw new InternalServerErrorException("Unable to perform verification: " + e.getMessage());
 920                 }
 921
 922                 String chainsFile = tempDir.getAbsolutePath() + "/chains.json";
 923                 generateChainsFile(graph, pathsWithMiddlebox, chainsFile);
 924
 925                 String configFile = tempDir.getAbsolutePath() + "/config.json";
 926                 generateConfigFile(graph, configFile);
 927
 928                 String traversalScenariosBasename = tempDir.getAbsolutePath() + "/TraversalScenario";
 929                 try{
 930                         generateTestScenarios(chainsFile, configFile, traversalScenariosBasename);
 931                 }catch(Exception ex){
 932                         testClassGenerator = generatorFolderForGrpc + "/test_class_generator.py";
 933                         generateTestScenarios(chainsFile, configFile, traversalScenariosBasename);
 934                 }
 935
 936                 String traversalTestsBasename = tempDir.getAbsolutePath() + "/TraversalTest";
 937                 try{
 938                         generateTests(  pathsWithMiddlebox.size(),
 939                                         traversalScenariosBasename,
 940                                         sourceNode.getName(),
 941                                         destinationNode.getName(),
 942                                         traversalTestsBasename);
 943                 }catch(InternalServerErrorException ex){
 944                         testGenerator = generatorFolderForGrpc + "/test_generator.py";
 945                         generateTests(  pathsWithMiddlebox.size(),
 946                                         traversalScenariosBasename,
 947                                         sourceNode.getName(),
 948                                         destinationNode.getName(),
 949                                         traversalTestsBasename);
 950                 }
 951                 List<File> sourceFiles = new ArrayList<File>();
 952                 List<File> classFiles = new ArrayList<File>();
 953                 prepareForCompilationAndExecution(      pathsWithMiddlebox.size(),
 954                                                                                         traversalScenariosBasename,
 955                                                                                         traversalTestsBasename,
 956                                                                                         sourceFiles,
 957                                                                                         classFiles);
 958
 959                 compileFiles(sourceFiles, tempDir.getAbsolutePath());
 960
 961                 tests = runFiles(tempDir.getAbsolutePath(), pathsWithMiddlebox, graph, classFiles);
 962
 963                 for (Test t : tests) {
 964                         if (t.getResult().equals("UNSAT")) {
 965                                 return new Verification("UNSAT",
 966                                                                                 tests,
 967                                                                                 "There is at least a path between '"    + sourceNode.getName() + "' and '"
 968                                                                                                 + destinationNode.getName() + "' traversing middlebox '"
 969                                                                                                 + middleboxNode.getName() + "' where '" + sourceNode.getName()
 970                                                                                                 + "' cannot reach '" + destinationNode.getName()
 971                                                                                                 + "'. See below the paths that have been checked");
 972                         }
 973                         if (t.getResult().equals("UNKNOWN")) {
 974                                 return new Verification("UNKNOWN",
 975                                                                                 tests,
 976                                                                                 "There is at least a path between '"    + sourceNode.getName() + "' and '"
 977                                                                                                 + destinationNode.getName() + "' traversing middlebox '"
 978                                                                                                 + middleboxNode.getName() + "' where it is not guaranteed that '"
 979                                                                                                 + sourceNode.getName() + "' can effectively reach '"
 980                                                                                                 + destinationNode.getName()
 981                                                                                                 + "'. See below the paths that have been checked");
 982                         }
 983                 }
 984
 985                 extractPathsWithoutMiddlebox(pathsBetweenSourceAndDestination, middleboxNode.getName());
 986                 printListsOfStrings("Paths without middlebox '" + middleboxNode.getName() + "'", pathsBetweenSourceAndDestination);
 987
 988                 if (pathsBetweenSourceAndDestination.isEmpty()) {
 989                         return new Verification("SAT",
 990                                                                         tests,
 991                                                                         "All the paths between node '"  + sourceNode.getName() + "' and '"
 992                                                                                         + destinationNode.getName() + "' traverse middlebox '"
 993                                                                                         + middleboxNode.getName() + "'");
 994                 }
 995
 996                 tempDir = null;
 997
 998                 try {
 999                         tempDir = createTempDir("traversal");
1000                 }
1001                 catch (IOException e) {
1002                         throw new InternalServerErrorException("Unable to perform verification: " + e.getMessage());
1003                 }
1004
1005                 chainsFile = tempDir.getAbsolutePath() + "/chains.json";
1006                 generateChainsFile(graph, pathsBetweenSourceAndDestination, chainsFile);
1007
1008                 configFile = tempDir.getAbsolutePath() + "/config.json";
1009                 generateConfigFile(graph, configFile);
1010
1011                 traversalScenariosBasename = tempDir.getAbsolutePath() + "/TraversalScenario";
1012                 generateTestScenarios(chainsFile, configFile, traversalScenariosBasename);
1013
1014                 traversalTestsBasename = tempDir.getAbsolutePath() + "/TraversalTest";
1015                 generateTests(  pathsBetweenSourceAndDestination.size(),
1016                                                 traversalScenariosBasename,
1017                                                 sourceNode.getName(),
1018                                                 destinationNode.getName(),
1019                                                 traversalTestsBasename);
1020
1021                 sourceFiles = new ArrayList<File>();
1022                 classFiles = new ArrayList<File>();
1023                 prepareForCompilationAndExecution(      pathsBetweenSourceAndDestination.size(),
1024                                                                                         traversalScenariosBasename,
1025                                                                                         traversalTestsBasename,
1026                                                                                         sourceFiles,
1027                                                                                         classFiles);
1028
1029                 compileFiles(sourceFiles, tempDir.getAbsolutePath());
1030
1031                 tests = runFiles(tempDir.getAbsolutePath(), pathsBetweenSourceAndDestination, graph, classFiles);
1032
1033                 return evaluateTraversalResults(tests,
1034                                                                                 sourceNode.getName(),
1035                                                                                 destinationNode.getName(),
1036                                                                                 middleboxNode.getName());
1037
1038         }
1039
1040         private Verification evaluateTraversalResults(  List<Test> tests, String source, String destination,
1041                                                                                                         String middlebox) {
1042                 Verification v = new Verification();
1043                 boolean isSat = false;
1044                 int unsatCounter = 0;
1045                 for (Test t : tests) {
1046                         v.getTests().add(t);
1047
1048                         if (t.getResult().equals("SAT")) {
1049                                 isSat = true;
1050                         }
1051                         else if (t.getResult().equals("UNKNOWN")) {
1052                                 v.setResult("UNKNWON");
1053                                 v.setComment("There is at least one path from '"        + source + "' to '" + destination
1054                                                                 + "' that doesn't traverse middlebox '" + middlebox
1055                                                                 + "' (see below all the paths that have been checked)");
1056                         }
1057                         else if (t.getResult().equals("UNSAT")) {
1058                                 unsatCounter++;
1059                         }
1060                 }
1061                 if (isSat) {
1062                         v.setResult("UNSAT");
1063                         v.setComment("There is at least one path from '"        + source + "' to '" + destination
1064                                                         + "' that doesn't traverse middlebox '" + middlebox
1065                                                         + "' (see below all the paths that have been checked)");
1066                 }
1067                 else if (unsatCounter == tests.size()) {
1068                         v.setResult("SAT");
1069                         v.setComment("The only available paths from '"  + source + "' to '" + destination
1070                                                         + "' are those that traverse middlebox '" + middlebox
1071                                                         + "' (see below the alternative paths that have been checked and are unusable)");
1072                 }
1073                 return v;
1074         }
1075
1076         private Verification reachabilityVerification(Graph graph, Node sourceNode, Node destinationNode) {
1077                 Paths paths = getPaths(graph, sourceNode, destinationNode);
1078
1079                 if (paths.getPath().size() == 0) {
1080                         return new Verification("UNSAT",
1081                                                                         "There are no available paths between '"        + sourceNode.getName() + "' and '"
1082                                                                                                 + destinationNode.getName() + "'");
1083                 }
1084
1085                 List<List<String>> sanitizedPaths = sanitizePaths(paths);
1086
1087                 printListsOfStrings("Before loops removal", sanitizedPaths);
1088
1089                 eliminateLoopsInPaths(sanitizedPaths);
1090
1091                 printListsOfStrings("After loops removal", sanitizedPaths);
1092
1093                 if (sanitizedPaths.isEmpty()) {
1094                         return new Verification("UNSAT",
1095                                                                         "There are no available paths between '"        + sourceNode.getName() + "' and '"
1096                                                                                                 + destinationNode.getName() + "'");
1097                 }
1098
1099                 File tempDir = null;
1100
1101                 try {
1102                         tempDir = createTempDir("reachability");
1103                 }
1104                 catch (IOException e) {
1105                         throw new InternalServerErrorException("Unable to perform verification: " + e.getMessage());
1106                 }
1107
1108                 String chainsFile = tempDir.getAbsolutePath() + "/chains.json";
1109                 generateChainsFile(graph, sanitizedPaths, chainsFile);
1110
1111                 String configFile = tempDir.getAbsolutePath() + "/config.json";
1112                 generateConfigFile(graph, configFile);
1113
1114                 String reachabilityScenariosBasename = tempDir.getAbsolutePath() + "/ReachabilityScenario";
1115                 try{
1116                         generateTestScenarios(chainsFile, configFile, reachabilityScenariosBasename);
1117                 }catch(InternalServerErrorException ex){
1118                         testClassGenerator = generatorFolderForGrpc + "/test_class_generator.py";
1119                         generateTestScenarios(chainsFile, configFile, reachabilityScenariosBasename);
1120                 }
1121
1122
1123                 String reachabilityTestsBasename = tempDir.getAbsolutePath() + "/ReachabilityTest";
1124                 try{
1125                         generateTests(  sanitizedPaths.size(),
1126                                         reachabilityScenariosBasename,
1127                                         sourceNode.getName(),
1128                                         destinationNode.getName(),
1129                                         reachabilityTestsBasename);
1130                 }catch(InternalServerErrorException ex){
1131                         testGenerator = generatorFolderForGrpc + "/test_generator.py";
1132                         generateTests(  sanitizedPaths.size(),
1133                                         reachabilityScenariosBasename,
1134                                         sourceNode.getName(),
1135                                         destinationNode.getName(),
1136                                         reachabilityTestsBasename);
1137                 }
1138                 List<File> sourceFiles = new ArrayList<File>();
1139                 List<File> classFiles = new ArrayList<File>();
1140                 prepareForCompilationAndExecution(      sanitizedPaths.size(),
1141                                                                                         reachabilityScenariosBasename,
1142                                                                                         reachabilityTestsBasename,
1143                                                                                         sourceFiles,
1144                                                                                         classFiles);
1145
1146                 compileFiles(sourceFiles, tempDir.getAbsolutePath());
1147
1148                 List<Test> tests = runFiles(tempDir.getAbsolutePath(), sanitizedPaths, graph, classFiles);
1149
1150                 return evaluateReachabilityResult(tests, sourceNode.getName(), destinationNode.getName());
1151         }
1152
1153         private Verification evaluateReachabilityResult(List<Test> tests, String source, String destination) {
1154                 Verification v = new Verification();
1155                 boolean sat = false;
1156                 int unsat = 0;
1157                 for (Test t : tests) {
1158                         v.getTests().add(t);
1159
1160                         if (t.getResult().equals("SAT")) {
1161                                 sat = true;
1162                         }
1163                         else if (t.getResult().equals("UNKNOWN")) {
1164                                 v.setResult("UNKNWON");
1165                                 v.setComment("Reachability from '"      + source + "' to '" + destination
1166                                                                 + "' is unknown. See all the checked paths below");
1167                         }
1168                         else if (t.getResult().equals("UNSAT")) {
1169                                 unsat++;
1170                         }
1171                 }
1172                 if (sat) {
1173                         v.setResult("SAT");
1174                         v.setComment("There is at least one path '"     + source + "' can use to reach '" + destination
1175                                                         + "'. See all the available paths below");
1176                 }
1177                 else if (unsat == tests.size()) {
1178                         v.setResult("UNSAT");
1179                         v.setComment("There isn't any path '"   + source + "' can use to reach '" + destination
1180                                                         + "'. See all the checked paths below");
1181                 }
1182                 return v;
1183         }
1184
1185 }