From a42de79292d9541db7865b54e93be2d0b6e6a094 Mon Sep 17 00:00:00 2001 From: "serena.spinoso" Date: Thu, 7 Sep 2017 10:22:39 +0200 Subject: update verigraph JIRA: PARSER-154 code optimizations about graph manipulation and formula generation. Change-Id: Idebef19b128281aa2bc40d1aeab6e208c7ddd93d Signed-off-by: serena.spinoso --- .../it/polito/verigraph/service/GraphService.java | 82 +++ .../verigraph/service/JsonValidationService.java | 132 +++++ .../polito/verigraph/service/NeighbourService.java | 143 +++++ .../it/polito/verigraph/service/NodeService.java | 223 ++++++++ .../polito/verigraph/service/ValidationUtils.java | 131 +++++ .../verigraph/service/VerificationService.java | 625 +++++++++++++++++++++ .../polito/verigraph/service/VerigraphLogger.java | 71 +++ 7 files changed, 1407 insertions(+) create mode 100644 verigraph/src/it/polito/verigraph/service/GraphService.java create mode 100644 verigraph/src/it/polito/verigraph/service/JsonValidationService.java create mode 100644 verigraph/src/it/polito/verigraph/service/NeighbourService.java create mode 100644 verigraph/src/it/polito/verigraph/service/NodeService.java create mode 100644 verigraph/src/it/polito/verigraph/service/ValidationUtils.java create mode 100644 verigraph/src/it/polito/verigraph/service/VerificationService.java create mode 100644 verigraph/src/it/polito/verigraph/service/VerigraphLogger.java (limited to 'verigraph/src/it/polito/verigraph/service') diff --git a/verigraph/src/it/polito/verigraph/service/GraphService.java b/verigraph/src/it/polito/verigraph/service/GraphService.java new file mode 100644 index 0000000..7e92281 --- /dev/null +++ b/verigraph/src/it/polito/verigraph/service/GraphService.java @@ -0,0 +1,82 @@ +/******************************************************************************* + * Copyright (c) 2017 Politecnico di Torino and others. + * + * All rights reserved. This program and the accompanying materials + * are made available under the terms of the Apache License, Version 2.0 + * which accompanies this distribution, and is available at + * http://www.apache.org/licenses/LICENSE-2.0 + *******************************************************************************/ +package it.polito.verigraph.service; + +import java.io.IOException; +import java.util.List; +import javax.xml.bind.JAXBException; +import com.fasterxml.jackson.core.JsonParseException; +import com.fasterxml.jackson.core.JsonProcessingException; +import com.fasterxml.jackson.databind.JsonMappingException; +import it.polito.neo4j.manager.Neo4jDBManager; +import it.polito.neo4j.exceptions.MyInvalidIdException; +import it.polito.neo4j.exceptions.MyNotFoundException; +import it.polito.verigraph.exception.ForbiddenException; +import it.polito.verigraph.model.Graph; +import it.polito.verigraph.model.Node; + +public class GraphService { + + private Neo4jDBManager manager= new Neo4jDBManager(); + public static VerigraphLogger vlogger = VerigraphLogger.getVerigraphlogger(); + + public GraphService() {} + + public List getAllGraphs() throws JsonProcessingException, MyNotFoundException { + List result; + result=manager.getGraphs(); + for(Graph g : result){ + validateGraph(g); + } + return result; + } + + public Graph getGraph(long id) throws JsonParseException, JsonMappingException, JAXBException, IOException { + if (id < 0) { + throw new ForbiddenException("Illegal graph id: " + id); + } + Graph localGraph=manager.getGraph(id); + validateGraph(localGraph); + return localGraph; + } + + public Graph updateGraph(Graph graph) throws JAXBException, JsonParseException, JsonMappingException, IOException, MyInvalidIdException { + if (graph.getId() < 0) { + throw new ForbiddenException("Illegal graph id: " + graph.getId()); + } + validateGraph(graph); + Graph localGraph=new Graph(); + localGraph=manager.updateGraph(graph); + vlogger.logger.info("Graph updated"); + validateGraph(localGraph); + return localGraph; + } + + + public void removeGraph(long id) { + + if (id < 0) { + throw new ForbiddenException("Illegal graph id: " + id); + } + manager.deleteGraph(id); + } + + public Graph addGraph(Graph graph) throws JAXBException, JsonParseException, JsonMappingException, IOException, MyInvalidIdException { + validateGraph(graph); + Graph g=manager.addGraph(graph); + validateGraph(g); + return g; + } + + public static void validateGraph(Graph graph) throws JsonProcessingException { + for (Node node : graph.getNodes().values()) { + NodeService.validateNode(graph, node); + } + } +} diff --git a/verigraph/src/it/polito/verigraph/service/JsonValidationService.java b/verigraph/src/it/polito/verigraph/service/JsonValidationService.java new file mode 100644 index 0000000..8f09a25 --- /dev/null +++ b/verigraph/src/it/polito/verigraph/service/JsonValidationService.java @@ -0,0 +1,132 @@ +/******************************************************************************* + * Copyright (c) 2017 Politecnico di Torino and others. + * + * All rights reserved. This program and the accompanying materials + * are made available under the terms of the Apache License, Version 2.0 + * which accompanies this distribution, and is available at + * http://www.apache.org/licenses/LICENSE-2.0 + *******************************************************************************/ +package it.polito.verigraph.service; + +import java.lang.reflect.InvocationTargetException; +import java.lang.reflect.Method; +import java.util.Iterator; +import java.util.Map.Entry; + +import org.apache.commons.lang3.text.WordUtils; + +import com.fasterxml.jackson.databind.JsonNode; + +import it.polito.verigraph.exception.BadRequestException; +import it.polito.verigraph.model.Graph; +import it.polito.verigraph.model.Node; + +public class JsonValidationService { + + private Graph graph= new Graph(); + private Node node= new Node(); + public static VerigraphLogger vlogger = VerigraphLogger.getVerigraphlogger(); + + public JsonValidationService() {} + + public JsonValidationService(Graph graph, Node node) { + this.graph = graph; + this.node = node; + } + + public boolean validateFieldAgainstNodeNames(String value) { + for (Node node : this.graph.getNodes().values()) { + if (node.getName().equals(value)) + return true; + } + return false; + } + + public void validateFieldsAgainstNodeNames(JsonNode node) { + if (node.isTextual()) { + boolean isValid = validateFieldAgainstNodeNames(node.asText()); + if (!isValid) { + vlogger.logger.info(node.asText() + " is not a valid string!"); + //System.out.println(node.asText() + " is not a valid string!"); + throw new BadRequestException("String '"+ node.asText() + + "' is not valid for the configuration of node '" + this.node.getName() + + "'"); + } + } + if (node.isArray()) { + for (JsonNode object : node) { + validateFieldsAgainstNodeNames(object); + } + } + if (node.isObject()) { + Iterator> iter = node.fields(); + while (iter.hasNext()) { + Entry item = iter.next(); + validateFieldsAgainstNodeNames(item.getValue()); + } + } + + } + + public boolean validateNodeConfiguration() { + String className = WordUtils.capitalize(node.getFunctional_type()) + "Validator"; + + Class validator; + try { + validator = Class.forName("it.polito.verigraph.validation." + className); + } + catch (ClassNotFoundException e) { + vlogger.logger.info(className+ " not found, configuration properties of node '" + node.getName() + + "' will be validated against node names"); + //System.out.println(className+ " not found, configuration properties of node '" + node.getName() + //+ "' will be validated against node names"); + return false; + } + + Class graphClass; + Class nodeClass; + Class configurationClass; + try { + graphClass = Class.forName("it.polito.verigraph.model.Graph"); + nodeClass = Class.forName("it.polito.verigraph.model.Node"); + configurationClass = Class.forName("it.polito.verigraph.model.Configuration"); + } + catch (ClassNotFoundException e) { + throw new RuntimeException("Model classes not found"); + } + + Class[] paramTypes = new Class[3]; + paramTypes[0] = graphClass; + paramTypes[1] = nodeClass; + paramTypes[2] = configurationClass; + String methodName = "validate"; + Object instance; + try { + instance = validator.newInstance(); + } + catch (InstantiationException e) { + throw new RuntimeException("'" + className + "' cannot be instantiated"); + } + catch (IllegalAccessException e) { + throw new RuntimeException("Illegal access to '" + className + "' instantiation"); + } + Method myMethod; + try { + myMethod = validator.getDeclaredMethod(methodName, paramTypes); + } + catch (NoSuchMethodException e) { + throw new RuntimeException("'" + methodName + "' method has to be implemented in " + className + " class"); + } + try { + myMethod.invoke(instance, graph, node, node.getConfiguration()); + } + catch (IllegalAccessException e) { + throw new RuntimeException("Illegal access to '" + methodName + "' method in " + className + " instance"); + } + catch (InvocationTargetException e) { + throw new BadRequestException("Validation failed for node '"+ node.getName() + "': " + + e.getTargetException().getMessage()); + } + return true; + } +} \ No newline at end of file diff --git a/verigraph/src/it/polito/verigraph/service/NeighbourService.java b/verigraph/src/it/polito/verigraph/service/NeighbourService.java new file mode 100644 index 0000000..ab557bf --- /dev/null +++ b/verigraph/src/it/polito/verigraph/service/NeighbourService.java @@ -0,0 +1,143 @@ +/******************************************************************************* + * Copyright (c) 2017 Politecnico di Torino and others. + * + * All rights reserved. This program and the accompanying materials + * are made available under the terms of the Apache License, Version 2.0 + * which accompanies this distribution, and is available at + * http://www.apache.org/licenses/LICENSE-2.0 + *******************************************************************************/ +package it.polito.verigraph.service; + +import java.io.IOException; +import java.util.ArrayList; +import java.util.List; +import java.util.Map; + +import javax.xml.bind.JAXBException; + +import com.fasterxml.jackson.core.JsonParseException; +import com.fasterxml.jackson.core.JsonProcessingException; +import com.fasterxml.jackson.databind.JsonMappingException; + +import it.polito.neo4j.manager.Neo4jDBManager; +import it.polito.verigraph.exception.BadRequestException; +import it.polito.verigraph.exception.DataNotFoundException; +import it.polito.verigraph.exception.ForbiddenException; +import it.polito.verigraph.model.Graph; +import it.polito.verigraph.model.Neighbour; +import it.polito.verigraph.model.Node; + +public class NeighbourService { + + private Neo4jDBManager manager=new Neo4jDBManager(); + + + public List getAllNeighbours(long graphId, long nodeId) throws JsonProcessingException { + if (graphId < 0) { + throw new ForbiddenException("Illegal graph id: " + graphId); + } + if (nodeId < 0) { + throw new ForbiddenException("Illegal node id: " + nodeId); + } + + Map neighbours = manager.getNeighbours(graphId, nodeId); + return new ArrayList(neighbours.values()); + } + + public Neighbour getNeighbour(long graphId, long nodeId, long neighbourId) throws JsonProcessingException { + if (graphId < 0) { + throw new ForbiddenException("Illegal graph id: " + graphId); + } + if (nodeId < 0) { + throw new ForbiddenException("Illegal node id: " + nodeId); + } + if (neighbourId < 0) { + throw new ForbiddenException("Illegal neighbour id: " + neighbourId); + } + + Neighbour neighbour=manager.getNeighbour(graphId, nodeId, neighbourId); + if (neighbour == null) { + throw new DataNotFoundException("Neighbour with id "+ neighbourId + " not found for node with id " + nodeId + + " in graph with id " + graphId); + } + return neighbour; + } + + public Neighbour addNeighbour(long graphId, long nodeId, Neighbour neighbour) throws JsonParseException, JsonMappingException, JAXBException, IOException { + if (graphId < 0) { + throw new ForbiddenException("Illegal graph id: " + graphId); + } + if (nodeId < 0) { + throw new ForbiddenException("Illegal node id: " + nodeId); + } + Graph graph = manager.getGraph(graphId); + Node node=manager.getNodeById(nodeId, graphId); + validateNeighbour(graph, node, neighbour); + Neighbour out=manager.addNeighbours(graphId, nodeId, neighbour); + validateNeighbour(graph, node, neighbour); + return out; + } + + public Neighbour updateNeighbour(long graphId, long nodeId, Neighbour neighbour) throws JAXBException, IOException { + if (graphId < 0) { + throw new ForbiddenException("Illegal graph id: " + graphId); + } + if (nodeId < 0) { + throw new ForbiddenException("Illegal node id: " + nodeId); + } + if (neighbour.getId() < 0) { + throw new ForbiddenException("Illegal neighbour id: " + nodeId); + } + Graph graph=manager.getGraph(graphId); + Node node=manager.getNodeById(nodeId, graphId); + if (node == null) { + throw new DataNotFoundException("Node with id " + nodeId + " not found in graph with id " + graphId); + } + + validateNeighbour(graph, node, neighbour); + Neighbour n=manager.updateNeighbour(graphId, nodeId, neighbour); + + return n; + } + + public Neighbour removeNeighbour(long graphId, long nodeId, long neighbourId) { + if (graphId < 0) { + throw new ForbiddenException("Illegal graph id: " + graphId); + } + if (nodeId < 0) { + throw new ForbiddenException("Illegal node id: " + nodeId); + } + if (neighbourId < 0) { + throw new ForbiddenException("Illegal neighbour id: " + nodeId); + } + + Neighbour n=manager.deleteNeighbour(graphId, nodeId, neighbourId); + return n; + } + + public static void validateNeighbour(Graph graph, Node node, Neighbour neighbour) throws JsonProcessingException { + if (graph == null) + throw new BadRequestException("Neighbour validation failed: cannot validate null graph"); + if (node == null) + throw new BadRequestException("Neighbour validation failed: cannot validate null node"); + if (neighbour == null) + throw new BadRequestException("Neighbour validation failed: cannot validate null neighbour"); + + if (neighbour.getName() == null) + throw new BadRequestException("Neighbour validation failed: neighbour 'name' field cannot be null"); + if (neighbour.getName().equals("")) + throw new BadRequestException("Neighbour validation failed: neighbour 'name' field cannot be an empty string"); + + //Node nodeFound = graph.searchNodeByName(neighbour.getName()); + + Node nodeFound=graph.searchNodeByName(neighbour.getName()); + if ((nodeFound == null) || (nodeFound.getName().equals(node.getName()))) + throw new BadRequestException("Neighbour validation failed: '"+ neighbour.getName() + + "' is not a valid name for a neighbour of node '" + node.getName() + "'"); + + Neighbour neighbourFound = node.searchNeighbourByName(neighbour.getName()); + if ((neighbourFound != null) && (neighbourFound.equals(neighbour) == false)) + throw new BadRequestException("Neighbour validation failed: node '"+ node.getName() + + "' already has a neighbour named '" + neighbour.getName() + "'"); + } +} \ No newline at end of file diff --git a/verigraph/src/it/polito/verigraph/service/NodeService.java b/verigraph/src/it/polito/verigraph/service/NodeService.java new file mode 100644 index 0000000..ffd6751 --- /dev/null +++ b/verigraph/src/it/polito/verigraph/service/NodeService.java @@ -0,0 +1,223 @@ +/******************************************************************************* + * Copyright (c) 2017 Politecnico di Torino and others. + * + * All rights reserved. This program and the accompanying materials + * are made available under the terms of the Apache License, Version 2.0 + * which accompanies this distribution, and is available at + * http://www.apache.org/licenses/LICENSE-2.0 + *******************************************************************************/ +package it.polito.verigraph.service; + +import java.io.File; +import java.io.IOException; +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import javax.ws.rs.InternalServerErrorException; +import javax.xml.bind.JAXBException; +import com.fasterxml.jackson.core.JsonParseException; +import com.fasterxml.jackson.core.JsonProcessingException; +import com.fasterxml.jackson.databind.JsonMappingException; +import com.fasterxml.jackson.databind.JsonNode; +import com.github.fge.jsonschema.core.exceptions.ProcessingException; +import com.github.fge.jsonschema.main.JsonSchema; +import it.polito.neo4j.exceptions.MyInvalidIdException; +import it.polito.neo4j.exceptions.MyNotFoundException; +import it.polito.neo4j.manager.Neo4jDBManager; +import it.polito.verigraph.exception.BadRequestException; +import it.polito.verigraph.exception.DataNotFoundException; +import it.polito.verigraph.exception.ForbiddenException; +import it.polito.verigraph.model.Configuration; +import it.polito.verigraph.model.Graph; +import it.polito.verigraph.model.Neighbour; +import it.polito.verigraph.model.Node; + +public class NodeService { + + private Neo4jDBManager manager=new Neo4jDBManager(); + + public NodeService() {} + + public List getAllNodes(long graphId) throws JsonParseException, JsonMappingException, JAXBException, IOException, MyNotFoundException { + if (graphId < 0) { + throw new ForbiddenException("Illegal graph id: " + graphId); + } + + /*il controllo sull'esistenza del grafo viene fatto all'interno della getNodes + + */ + + Map nodes =manager.getNodes(graphId); + return new ArrayList(nodes.values()); + } + + public Node getNode(long graphId, long nodeId) throws JsonParseException, JsonMappingException, JAXBException, IOException, MyNotFoundException { + if (graphId < 0) { + throw new ForbiddenException("Illegal graph id: " + graphId); + } + if (nodeId < 0) { + throw new ForbiddenException("Illegal node id: " + nodeId); + } + + Node node=manager.getNodeById(nodeId, graphId); + if (node == null) { + throw new DataNotFoundException("Node with id " + nodeId + " not found in graph with id " + graphId); + } + return node; + } + + public Node updateNode(long graphId, Node node) throws JAXBException, IOException, MyInvalidIdException { + if (graphId < 0) { + throw new ForbiddenException("Illegal graph id: " + graphId); + } + if (node.getId() < 0) { + throw new ForbiddenException("Illegal node id: " + node.getId()); + } + + Graph graph=manager.getGraph(graphId); + validateNode(graph, node); + + Node n=manager.updateNode(graphId, node, node.getId()); + validateNode(graph, n); + + return n; + } + + public Node removeNode(long graphId, long nodeId) throws JsonParseException, JsonMappingException, JAXBException, IOException { + if (graphId < 0) { + throw new ForbiddenException("Illegal graph id: " + graphId); + } + if (nodeId < 0) { + throw new ForbiddenException("Illegal node id: " + nodeId); + } + + Graph graph=manager.getGraph(graphId); + if (graph == null) + throw new DataNotFoundException("Graph with id " + graphId + " not found"); + Node n=manager.deleteNode(graphId, nodeId); + return n; + } + + public Node addNode(long graphId, Node node) throws JsonParseException, JsonMappingException, JAXBException, IOException, MyInvalidIdException { + if (graphId < 0) { + throw new ForbiddenException("Illegal graph id: " + graphId); + } + + Graph graph=manager.getGraph(graphId); + validateNode(graph, node); + Node n=manager.addNode(graphId, node); + validateNode(graph, n); + return n; + } + + public Node searchByName(long graphId, String nodeName) throws JsonParseException, JsonMappingException, JAXBException, IOException { + if (graphId < 0) { + throw new ForbiddenException("Illegal graph id: " + graphId); + } + Graph graph = manager.getGraph(graphId); + if (graph == null) + throw new DataNotFoundException("Graph with id " + graphId + " not found"); + Map nodes = graph.getNodes(); + for (Node node : nodes.values()) { + if (node.getName().equals(nodeName)) + return node; + } + return null; + } + + public static void validateNode(Graph graph, Node node) throws JsonProcessingException { + if (graph == null) + throw new BadRequestException("Node validation failed: cannot validate null graph"); + if (node == null) + throw new BadRequestException("Node validation failed: cannot validate null node"); + + if (node.getName() == null) + throw new BadRequestException("Node validation failed: node 'name' field cannot be null"); + if (node.getFunctional_type() == null) + throw new BadRequestException("Node validation failed: node 'functional_type' field cannot be null"); + + if (node.getName().equals("")) + throw new BadRequestException("Node validation failed: node 'name' field cannot be an empty string"); + if (node.getFunctional_type().equals("")) + throw new BadRequestException("Node validation failed: node 'functional_type' field cannot be an empty string"); + + Node nodeFound =graph.searchNodeByName(node.getName()); + if ((nodeFound != null) && (nodeFound.equals(node) == false)) + throw new BadRequestException("Node validation failed: graph already has a node named '"+ node.getName() + + "'"); + Configuration configuration = node.getConfiguration(); + if (configuration != null) { + JsonNode configurationJsonNode = configuration.getConfiguration(); + // validate configuration against schema file + validateNodeConfigurationAgainstSchemaFile(node, configurationJsonNode); + JsonValidationService jsonValidator = new JsonValidationService(graph, node); + boolean hasCustomValidator = jsonValidator.validateNodeConfiguration(); + if (!hasCustomValidator) { + jsonValidator.validateFieldsAgainstNodeNames(configurationJsonNode); + } + } + + // validate neighbours + Map nodeNeighboursMap = node.getNeighbours(); + if (nodeNeighboursMap == null) + throw new BadRequestException("Node validation failed: node 'neighbours' cannot be null"); + for (Neighbour neighbour : nodeNeighboursMap.values()) { + NeighbourService.validateNeighbour(graph, node, neighbour); + } + } + + public static void validateNodeConfigurationAgainstSchemaFile(Node node, JsonNode configurationJson) { + String schemaFileName = node.getFunctional_type() + ".json"; + + File schemaFile = new File(System.getProperty("catalina.base") + "/webapps/verigraph/jsonschema/" + schemaFileName); + + if (!schemaFile.exists()) { + //if no REST client, try gRPC application + schemaFile = new File(System.getProperty("user.dir") + "/jsonschema/" + schemaFileName); + + if (!schemaFile.exists()) { + throw new ForbiddenException("Functional type '"+ node.getFunctional_type() + + "' is not supported! Please edit 'functional_type' field of node '" + + node.getName() + "'"); + } + } + + JsonSchema schemaNode = null; + try { + schemaNode = ValidationUtils.getSchemaNode(schemaFile); + } + catch (IOException e) { + throw new InternalServerErrorException("Unable to load '" + schemaFileName + "' schema file"); + } + catch (ProcessingException e) { + throw new InternalServerErrorException("Unable to resolve '"+ schemaFileName + + "' schema file as a schema node"); + } + + try { + ValidationUtils.validateJson(schemaNode, configurationJson); + } + catch (ProcessingException e) { + throw new BadRequestException("Something went wrong trying to validate node '"+ node.getName() + + "' with the following configuration: '" + configurationJson.toString() + + "' against the json schema '" + schemaFile.getName() + "': " + + e.getMessage()); + } + + } + + public Configuration addNodeConfiguration(long graphId, long nodeId, Configuration nodeConfiguration) throws IOException, MyInvalidIdException { + if (graphId < 0) { + throw new ForbiddenException("Illegal graph id: " + graphId); + } + if (nodeId < 0) { + throw new ForbiddenException("Illegal node id: " + nodeId); + } + + Node node=manager.getNodeById(nodeId, graphId); + validateNodeConfigurationAgainstSchemaFile(node, nodeConfiguration.getConfiguration()); + Configuration newConf=manager.updateConfiguration(nodeId, graphId, nodeConfiguration, node); + return newConf; + } +} \ No newline at end of file diff --git a/verigraph/src/it/polito/verigraph/service/ValidationUtils.java b/verigraph/src/it/polito/verigraph/service/ValidationUtils.java new file mode 100644 index 0000000..d64b544 --- /dev/null +++ b/verigraph/src/it/polito/verigraph/service/ValidationUtils.java @@ -0,0 +1,131 @@ +/******************************************************************************* + * Copyright (c) 2017 Politecnico di Torino and others. + * + * All rights reserved. This program and the accompanying materials + * are made available under the terms of the Apache License, Version 2.0 + * which accompanies this distribution, and is available at + * http://www.apache.org/licenses/LICENSE-2.0 + *******************************************************************************/ +package it.polito.verigraph.service; + +import java.io.File; +import java.io.IOException; +import java.net.URL; + +import com.fasterxml.jackson.databind.JsonNode; +import com.fasterxml.jackson.databind.node.ObjectNode; +import com.github.fge.jackson.JsonLoader; +import com.github.fge.jsonschema.core.exceptions.ProcessingException; +import com.github.fge.jsonschema.core.report.ProcessingMessage; +import com.github.fge.jsonschema.core.report.ProcessingReport; +import com.github.fge.jsonschema.main.JsonSchema; +import com.github.fge.jsonschema.main.JsonSchemaFactory; + +public class ValidationUtils { + + public static final String JSON_V4_SCHEMA_IDENTIFIER= "http://json-schema.org/draft-04/schema#"; + public static final String JSON_SCHEMA_IDENTIFIER_ELEMENT= "$schema"; + + public static JsonNode getJsonNode(String jsonText) throws IOException { + return JsonLoader.fromString(jsonText); + } // getJsonNode(text) ends + + public static JsonNode getJsonNode(File jsonFile) throws IOException { + return JsonLoader.fromFile(jsonFile); + } // getJsonNode(File) ends + + public static JsonNode getJsonNode(URL url) throws IOException { + return JsonLoader.fromURL(url); + } // getJsonNode(URL) ends + + public static JsonNode getJsonNodeFromResource(String resource) throws IOException { + return JsonLoader.fromResource(resource); + } // getJsonNode(Resource) ends + + public static JsonSchema getSchemaNode(String schemaText) throws IOException, ProcessingException { + final JsonNode schemaNode = getJsonNode(schemaText); + return _getSchemaNode(schemaNode); + } // getSchemaNode(text) ends + + public static JsonSchema getSchemaNode(File schemaFile) throws IOException, ProcessingException { + final JsonNode schemaNode = getJsonNode(schemaFile); + return _getSchemaNode(schemaNode); + } // getSchemaNode(File) ends + + public static JsonSchema getSchemaNode(URL schemaFile) throws IOException, ProcessingException { + final JsonNode schemaNode = getJsonNode(schemaFile); + return _getSchemaNode(schemaNode); + } // getSchemaNode(URL) ends + + public static JsonSchema getSchemaNodeFromResource(String resource) throws IOException, ProcessingException { + final JsonNode schemaNode = getJsonNodeFromResource(resource); + return _getSchemaNode(schemaNode); + } // getSchemaNode() ends + + public static void validateJson(JsonSchema jsonSchemaNode, JsonNode jsonNode) throws ProcessingException { + ProcessingReport report = jsonSchemaNode.validate(jsonNode); + if (!report.isSuccess()) { + for (ProcessingMessage processingMessage : report) { + throw new ProcessingException(processingMessage); + } + } + } // validateJson(Node) ends + + public static boolean isJsonValid(JsonSchema jsonSchemaNode, JsonNode jsonNode) throws ProcessingException { + ProcessingReport report = jsonSchemaNode.validate(jsonNode); + return report.isSuccess(); + } // validateJson(Node) ends + + public static boolean isJsonValid(String schemaText, String jsonText) throws ProcessingException, IOException { + final JsonSchema schemaNode = getSchemaNode(schemaText); + final JsonNode jsonNode = getJsonNode(jsonText); + return isJsonValid(schemaNode, jsonNode); + } // validateJson(Node) ends + + public static boolean isJsonValid(File schemaFile, File jsonFile) throws ProcessingException, IOException { + final JsonSchema schemaNode = getSchemaNode(schemaFile); + final JsonNode jsonNode = getJsonNode(jsonFile); + return isJsonValid(schemaNode, jsonNode); + } // validateJson(Node) ends + + public static boolean isJsonValid(URL schemaURL, URL jsonURL) throws ProcessingException, IOException { + final JsonSchema schemaNode = getSchemaNode(schemaURL); + final JsonNode jsonNode = getJsonNode(jsonURL); + return isJsonValid(schemaNode, jsonNode); + } // validateJson(Node) ends + + public static void validateJson(String schemaText, String jsonText) throws IOException, ProcessingException { + final JsonSchema schemaNode = getSchemaNode(schemaText); + final JsonNode jsonNode = getJsonNode(jsonText); + validateJson(schemaNode, jsonNode); + } // validateJson(text) ends + + public static void validateJson(File schemaFile, File jsonFile) throws IOException, ProcessingException { + final JsonSchema schemaNode = getSchemaNode(schemaFile); + final JsonNode jsonNode = getJsonNode(jsonFile); + validateJson(schemaNode, jsonNode); + } // validateJson(File) ends + + public static void validateJson(URL schemaDocument, URL jsonDocument) throws IOException, ProcessingException { + final JsonSchema schemaNode = getSchemaNode(schemaDocument); + final JsonNode jsonNode = getJsonNode(jsonDocument); + validateJson(schemaNode, jsonNode); + } // validateJson(URL) ends + + public static void validateJsonResource(String schemaResource, String jsonResource)throws IOException, + ProcessingException { + final JsonSchema schemaNode = getSchemaNode(schemaResource); + final JsonNode jsonNode = getJsonNodeFromResource(jsonResource); + validateJson(schemaNode, jsonNode); + } // validateJsonResource() ends + + private static JsonSchema _getSchemaNode(JsonNode jsonNode) throws ProcessingException { + final JsonNode schemaIdentifier = jsonNode.get(JSON_SCHEMA_IDENTIFIER_ELEMENT); + if (null == schemaIdentifier) { + ((ObjectNode) jsonNode).put(JSON_SCHEMA_IDENTIFIER_ELEMENT, JSON_V4_SCHEMA_IDENTIFIER); + } + + final JsonSchemaFactory factory = JsonSchemaFactory.byDefault(); + return factory.getJsonSchema(jsonNode); + } // _getSchemaNode() ends +} \ No newline at end of file diff --git a/verigraph/src/it/polito/verigraph/service/VerificationService.java b/verigraph/src/it/polito/verigraph/service/VerificationService.java new file mode 100644 index 0000000..227ea4b --- /dev/null +++ b/verigraph/src/it/polito/verigraph/service/VerificationService.java @@ -0,0 +1,625 @@ +/******************************************************************************* + * Copyright (c) 2017 Politecnico di Torino and others. + * + * All rights reserved. This program and the accompanying materials + * are made available under the terms of the Apache License, Version 2.0 + * which accompanies this distribution, and is available at + * http://www.apache.org/licenses/LICENSE-2.0 + *******************************************************************************/ +package it.polito.verigraph.service; + +import java.io.IOException; +import java.util.Date; +import java.util.ArrayList; +import java.util.Calendar; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.logging.Logger; +import java.util.regex.Matcher; +import java.util.regex.Pattern; +import java.util.stream.Collectors; +import javax.xml.bind.JAXBException; +import com.fasterxml.jackson.core.JsonParseException; +import com.fasterxml.jackson.databind.JsonMappingException; +import com.microsoft.z3.*; +import it.polito.neo4j.exceptions.MyInvalidDirectionException; +import it.polito.neo4j.jaxb.Paths; +import it.polito.neo4j.manager.Neo4jDBManager; +import it.polito.neo4j.manager.Neo4jLibrary; +import it.polito.neo4j.translator.*; +import it.polito.verigraph.exception.BadRequestException; +import it.polito.verigraph.exception.DataNotFoundException; +import it.polito.verigraph.exception.ForbiddenException; +import it.polito.verigraph.model.Graph; +import it.polito.verigraph.model.Node; +import it.polito.verigraph.model.Test; +import it.polito.verigraph.model.Verification; +import it.polito.verigraph.resources.beans.VerificationBean; +import it.polito.verigraph.solver.GeneratorSolver; +import it.polito.verigraph.solver.Scenario; + +public class VerificationService { + + private Neo4jDBManager manager=new Neo4jDBManager(); + //private final static Logger LOGGER = Logger.getLogger(VerigraphLogger.class.getName()); + public static VerigraphLogger vlogger = VerigraphLogger.getVerigraphlogger(); + + public VerificationService() {} + + private Paths getPaths(Graph graph, Node sourceNode, Node destinationNode) throws MyInvalidDirectionException { + + String source = sourceNode.getName(); + String destination = destinationNode.getName(); + Paths paths; + paths=manager.getPath(graph.getId(), source, destination, "outgoing"); + return paths; + } + + private List> sanitizePaths(Paths paths) { + List> sanitizedPaths = new ArrayList>(); + for (String path : paths.getPath()) { + List newPath = extractPath(path); + sanitizedPaths.add(newPath); + } + return sanitizedPaths; + } + + private List extractPath(String path) { + List newPath = new ArrayList(); + // find all nodes, i.e. all names between parentheses + Matcher m = Pattern.compile("\\(([^)]+)\\)").matcher(path); + while (m.find()) { + String node = m.group(1); + newPath.add(node); + } + return newPath; + } + + private void printListsOfStrings(String message, List> lists) { + vlogger.logger.info(message); + for (List element : lists) { + StringBuilder paths= new StringBuilder(); + for(String s : element){ + paths.append(s+" "); + } + vlogger.logger.info(paths.toString()); + //System.out.println(element); + } + } + + public Verification verify(long graphId, VerificationBean verificationBean) throws MyInvalidDirectionException, JsonParseException, JsonMappingException, JAXBException, IOException { + if (graphId < 0) { + throw new ForbiddenException("Illegal graph id: " + graphId); + } + GraphService graphService = new GraphService(); + Graph graph = graphService.getGraph(graphId); + if (graph == null) { + throw new DataNotFoundException("Graph with id " + graphId + " not found"); + } + String source = verificationBean.getSource(); + String destination = verificationBean.getDestination(); + String type = verificationBean.getType(); + if (source == null || source.equals("")) { + throw new BadRequestException("Please specify the 'source' parameter in your request"); + } + if (destination == null || destination.equals("")) { + throw new BadRequestException("Please specify the 'destination' parameter in your request"); + } + if (type == null || type.equals("")) { + throw new BadRequestException("Please specify the 'type' parameter in your request"); + } + + Node sourceNode = graph.searchNodeByName(verificationBean.getSource()); + Node destinationNode = graph.searchNodeByName(verificationBean.getDestination()); + + if (sourceNode == null) { + throw new BadRequestException("The 'source' parameter '" + source + "' is not valid, please insert the name of an existing node"); + } + if (destinationNode == null) { + throw new BadRequestException("The 'destination' parameter '" + destination + "' is not valid, please insert the name of an existing node"); + } + if ((!type.equals("reachability")) && (!type.equals("isolation")) && (!type.equals("traversal"))) { + throw new BadRequestException("The 'type' parameter '"+ type + + "' is not valid: valid types are: 'reachability', 'isolation' and 'traversal'"); + } + + Verification v = null; + String middlebox; + Node middleboxNode; + switch (type) { + case "reachability": + v = reachabilityVerification(graph, sourceNode, destinationNode); + break; + case "isolation": + middlebox = verificationBean.getMiddlebox(); + if (middlebox == null || middlebox.equals("")) { + throw new BadRequestException("Please specify the 'middlebox' parameter in your request"); + } + + middleboxNode = graph.searchNodeByName(middlebox); + if (middleboxNode == null) { + throw new BadRequestException("The 'middlebox' parameter '" + middlebox + "' is not valid, please insert the name of an existing node"); + } + if (middleboxNode.getFunctional_type().equals("endpoint")) { + throw new BadRequestException("'"+ middlebox + + "' is of type 'endpoint', please choose a valid middlebox"); + } + v = isolationVerification(graph, sourceNode, destinationNode, middleboxNode); + break; + case "traversal": + middlebox = verificationBean.getMiddlebox(); + if (middlebox == null || middlebox.equals("")) { + throw new BadRequestException("Please specify the 'middlebox' parameter in your request"); + } + + middleboxNode = graph.searchNodeByName(middlebox); + if (middleboxNode == null) { + throw new BadRequestException("The 'middlebox' parameter '" + middlebox + "' is not valid, please insert the name of an existing node"); + } + if (middleboxNode.getFunctional_type().equals("endpoint")) { + throw new BadRequestException("'"+ middlebox + + "' is of type 'endpoint', please choose a valid middlebox"); + } + v = traversalVerification(graph, sourceNode, destinationNode, middleboxNode); + break; + default: + break; + } + return v; + } + + private Verification isolationVerification(Graph graph, Node sourceNode, Node destinationNode, Node middleboxNode) throws MyInvalidDirectionException { + Long time_isolation=(long) 0; + Calendar cal_isolation = Calendar.getInstance(); + Date start_time_isolation = cal_isolation.getTime(); + Paths paths = getPaths(graph, sourceNode, destinationNode); + if (paths.getPath().size() == 0) { + return new Verification("UNSAT", + "There are no available paths between '"+ sourceNode.getName() + "' and '" + + destinationNode.getName() + "'"); + } + + List> sanitizedPaths = sanitizePaths(paths); + List tests = extractTestsFromPaths(graph, sanitizedPaths, "UNKNWON"); + + //printListsOfStrings("sanitizedPaths", sanitizedPaths); + + if (sanitizedPaths.isEmpty()) { + return new Verification("UNSAT", + "There are no available paths between '"+ sourceNode.getName() + "' and '" + + destinationNode.getName() + "'"); + } + extractPathsWithoutMiddlebox(sanitizedPaths, middleboxNode.getName()); + + if (sanitizedPaths.isEmpty()) { + return new Verification("UNSAT", + tests, + "There are no available paths between '"+ sourceNode.getName() + "' and '" + + destinationNode.getName() + "' which no traverse middlebox '" + + middleboxNode.getName() + "'. See below all the available paths."); + } + + //printListsOfStrings("Paths with middlebox '" + middleboxNode.getName() + "'", sanitizedPaths); + + Map scenarios=createScenarios(sanitizedPaths, graph); + + tests = run(graph, scenarios, sourceNode.getName(), destinationNode.getName()); + Verification isolation=evaluateIsolationResults(tests, sourceNode.getName(), + destinationNode.getName(), + middleboxNode.getName()); + Calendar cal_isolation_stop = Calendar.getInstance(); + time_isolation = time_isolation +(cal_isolation_stop.getTime().getTime() - start_time_isolation.getTime()); + vlogger.logger.info("Time to check reachability policy: " + time_isolation); + //System.out.println("Time to check reachability policy: " + time_isolation); + return isolation; + } + + private List extractTestsFromPaths(Graph graph, List> paths, String result) { + List tests = new ArrayList(); + for (List path : paths) { + List nodes = new ArrayList(); + for (String nodeName : path) { + nodes.add(graph.searchNodeByName(nodeName)); + } + tests.add(new Test(nodes, result)); + } + return tests; + } + + private Verification evaluateIsolationResults(List tests, String source, String destination, + String middlebox) { + Verification v = new Verification(); + boolean isSat = false; + int unsatCounter = 0; + for (Test t : tests) { + v.getTests().add(t); + if (t.getResult().equals("SAT")) { + isSat = true; + } + else if (t.getResult().equals("UNKNOWN")) { + v.setResult("UNKNOWN"); + v.setComment("Isolation property with source '"+ source + "', destination '" + destination + + "' and middlebox '" + middlebox + "' is UNKNOWN because although '" + source + + "' cannot reach '" + middlebox + "' in any path from '" + source + "' to '" + + destination + "' which traverses middlebox '" + middlebox + + "' at least one reachability test between '" + source + "' and '" + middlebox + + "' returned UNKNOWN (see below all the paths that have been checked)"); + } + else if (t.getResult().equals("UNSAT")) { + unsatCounter++; + } + } + if (isSat) { + v.setResult("SAT"); + v.setComment("Isolation property with source '"+ source + "', destination '" + destination + + "' and middlebox '" + middlebox + "' is SATISFIED because reachability between '" + source + + "' and '" + middlebox + "' is UNSATISFIED in all paths between '" + source + "' and '" + + destination + "' which traverse middlebox '" + middlebox + + "' (see below all the paths that have been checked)"); + + } + else if (unsatCounter == tests.size()) { + v.setResult("UNSAT"); + v.setComment("Isolation property with source '"+ source + "', destination '" + destination + + "' and middlebox '" + middlebox + "' is UNSATISFIED because reachability between '" + + source + "' and '" + middlebox + "' is SATISFIED in at least one path between '" + source + + "' and '" + destination + "' which traverses middlebox '" + middlebox + + "' (see below all the paths that have been checked)"); + } + return v; + } + + private void extractPathsWithMiddlebox(List> sanitizedPaths, String middleboxName) { + List> pathsToBeRemoved = new ArrayList>(); + for (List path : sanitizedPaths) { + boolean middleboxFound = false; + for (String node : path) { + if (node.equals(middleboxName)) { + middleboxFound = true; + break; + } + } + if (!middleboxFound) { + pathsToBeRemoved.add(path); + } + } + for (List path : pathsToBeRemoved) { + sanitizedPaths.remove(path); + } + + } + + private void extractPathsWithoutMiddlebox(List> sanitizedPaths, String middleboxName) { + List> pathsToBeRemoved = new ArrayList>(); + for (List path : sanitizedPaths) { + boolean middleboxFound = false; + for (String node : path) { + if (node.equals(middleboxName)) { + middleboxFound = true; + break; + } + } + if (middleboxFound) { + pathsToBeRemoved.add(path); + } + } + for (List path : pathsToBeRemoved) { + sanitizedPaths.remove(path); + } + } + + private Verification traversalVerification(Graph graph, Node sourceNode, Node destinationNode, Node middleboxNode) throws MyInvalidDirectionException { + Long time_traversal=(long) 0; + Calendar cal_traversal = Calendar.getInstance(); + Date start_time_traversal = cal_traversal.getTime(); + Paths paths = getPaths(graph, sourceNode, destinationNode); + if (paths.getPath().size() == 0) { + return new Verification("UNSAT", + "There are no available paths between '"+ sourceNode.getName() + "' and '" + + destinationNode.getName() + "'"); + } + + List> pathsBetweenSourceAndDestination = sanitizePaths(paths); + + //printListsOfStrings("Paths", pathsBetweenSourceAndDestination); + + if (pathsBetweenSourceAndDestination.isEmpty()) { + return new Verification("UNSAT", + "There are no available paths between '"+ sourceNode.getName() + "' and '" + + destinationNode.getName() + "'"); + } + + List tests = extractTestsFromPaths(graph, pathsBetweenSourceAndDestination, "UNKNOWN"); + + List> pathsWithMiddlebox = new ArrayList>(); + for (List path : pathsBetweenSourceAndDestination) { + pathsWithMiddlebox.add(path); + } + + extractPathsWithMiddlebox(pathsWithMiddlebox, middleboxNode.getName()); + + if (pathsWithMiddlebox.isEmpty()) { + return new Verification("UNSAT", + tests, + "There are no paths between '"+ sourceNode.getName() + "' and '" + + destinationNode.getName() + "' which traverse middlebox '" + + middleboxNode.getName() + "'. See below all the available paths"); + } + + //printListsOfStrings("Paths with middlebox '" + middleboxNode.getName() + "'", pathsWithMiddlebox); + + Map scenarios=createScenarios(pathsWithMiddlebox, graph); + + tests = run(graph, scenarios, sourceNode.getName(), destinationNode.getName()); + + for (Test t : tests) { + if (t.getResult().equals("UNSAT")) { + return new Verification("UNSAT", + tests, + "There is at least a path between '"+ sourceNode.getName() + "' and '" + + destinationNode.getName() + "' traversing middlebox '" + + middleboxNode.getName() + "' where '" + sourceNode.getName() + + "' cannot reach '" + destinationNode.getName() + + "'. See below the paths that have been checked"); + } + if (t.getResult().equals("UNKNOWN")) { + return new Verification("UNKNOWN", + tests, + "There is at least a path between '"+ sourceNode.getName() + "' and '" + + destinationNode.getName() + "' traversing middlebox '" + + middleboxNode.getName() + "' where it is not guaranteed that '" + + sourceNode.getName() + "' can effectively reach '" + + destinationNode.getName() + + "'. See below the paths that have been checked"); + } + } + + extractPathsWithoutMiddlebox(pathsBetweenSourceAndDestination, middleboxNode.getName()); + printListsOfStrings("Paths without middlebox '" + middleboxNode.getName() + "'", pathsBetweenSourceAndDestination); + + if (pathsBetweenSourceAndDestination.isEmpty()) { + return new Verification("SAT", + tests, + "All the paths between node '"+ sourceNode.getName() + "' and '" + + destinationNode.getName() + "' traverse middlebox '" + + middleboxNode.getName() + "'"); + } + + + Map scenarios2=createScenarios( pathsBetweenSourceAndDestination, graph); + + tests = run(graph, scenarios2, sourceNode.getName(), destinationNode.getName()); + + Verification traversal= evaluateTraversalResults(tests, + sourceNode.getName(), + destinationNode.getName(), + middleboxNode.getName()); + + Calendar cal_traversal_stop = Calendar.getInstance(); + time_traversal = time_traversal +(cal_traversal_stop.getTime().getTime() - start_time_traversal.getTime()); + vlogger.logger.info("Time to check traversal policy: " + time_traversal); + //System.out.println("Time to check traversal policy: " + time_traversal); + return traversal; + } + + private Verification evaluateTraversalResults(List tests, String source, String destination, + String middlebox) { + Verification v = new Verification(); + boolean isSat = false; + int unsatCounter = 0; + for (Test t : tests) { + v.getTests().add(t); + + if (t.getResult().equals("SAT")) { + isSat = true; + } + else if (t.getResult().equals("UNKNOWN")) { + v.setResult("UNKNWON"); + v.setComment("There is at least one path from '"+ source + "' to '" + destination + + "' that doesn't traverse middlebox '" + middlebox + + "' (see below all the paths that have been checked)"); + } + else if (t.getResult().equals("UNSAT")) { + unsatCounter++; + } + } + if (isSat) { + v.setResult("UNSAT"); + v.setComment("There is at least one path from '"+ source + "' to '" + destination + + "' that doesn't traverse middlebox '" + middlebox + + "' (see below all the paths that have been checked)"); + } + else if (unsatCounter == tests.size()) { + v.setResult("SAT"); + v.setComment("The only available paths from '"+ source + "' to '" + destination + + "' are those that traverse middlebox '" + middlebox + + "' (see below the alternative paths that have been checked and are unusable)"); + } + return v; + } + + private Verification reachabilityVerification(Graph graph, Node sourceNode, Node destinationNode) throws MyInvalidDirectionException { + Long time_reachability=(long) 0; + Calendar cal_reachability = Calendar.getInstance(); + Date start_time_reachability = cal_reachability.getTime(); + + Paths paths = getPaths(graph, sourceNode, destinationNode); + + if (paths.getPath().size() == 0) { + return new Verification("UNSAT", + "There are no available paths between '"+ sourceNode.getName() + "' and '" + + destinationNode.getName() + "'"); + } + + List> sanitizedPaths = sanitizePaths(paths); + + printListsOfStrings("Paths", sanitizedPaths); + + if (sanitizedPaths.isEmpty()) { + return new Verification("UNSAT", + "There are no available paths between '"+ sourceNode.getName() + "' and '" + + destinationNode.getName() + "'"); + } + + Map scenarios=createScenarios(sanitizedPaths, graph); + + List tests = run(graph, scenarios, sourceNode.getName(), destinationNode.getName()); + + Calendar cal_reachability_after_run = Calendar.getInstance(); + time_reachability = time_reachability +(cal_reachability_after_run.getTime().getTime() - start_time_reachability.getTime()); + vlogger.logger.info("Time reachability after run: " + time_reachability); + //System.out.println("Time reachability after run: " + time_reachability); + + Verification reachability= evaluateReachabilityResult(tests, sourceNode.getName(), destinationNode.getName()); + + Calendar cal_reachability_stop = Calendar.getInstance(); + time_reachability = time_reachability +(cal_reachability_stop.getTime().getTime() - start_time_reachability.getTime()); + vlogger.logger.info("Time to check reachability policy: " + time_reachability); + //System.out.println("Time to check reachability policy: " + time_reachability); + + return reachability; + } + + private List run(Graph graph, Map scenarios, String src, String dst) { + List tests = new ArrayList(); + String result; + + //estimation time + //Long time=(long) 0; + //Calendar cal = Calendar.getInstance(); + //Date start_time = cal.getTime(); + + for(Map.Entry t : scenarios.entrySet()){ + + result=t.getValue().run(src, dst); + + List path = new ArrayList(); + for (String nodeString : t.getValue().getPaths()) { + Node node = graph.searchNodeByName(nodeString); + path.add(node); + } + Test test = new Test(path, result); + tests.add(test); + } + + //Calendar cal2 = Calendar.getInstance(); + //time = time +(cal2.getTime().getTime() - start_time.getTime()); + //System.out.println("Time occur to run: " + time); + + return tests; + } + + private Map createScenarios(List> sanitizedPaths, Graph graph) { + int index=0; + Map scenarios=new HashMap(); + for(List s : sanitizedPaths){ + Scenario tmp=new Scenario(graph, s); + tmp.createScenario(); + GeneratorSolver gs=new GeneratorSolver(tmp, s); + gs.genSolver(); + scenarios.put(index++, gs); + } + return scenarios; + } + + private Verification evaluateReachabilityResult(List tests, String source, String destination) { + Verification v = new Verification(); + boolean sat = false; + int unsat = 0; + for (Test t : tests) { + + if (t.getResult().equals("SAT")) { + sat = true; + } + + else if (t.getResult().equals("UNKNOWN")) { + v.setResult("UNKNWON"); + v.setComment("Reachability from '"+ source + "' to '" + destination + + "' is unknown. See all the checked paths below"); + + } + else if (t.getResult().equals("UNSAT")) { + unsat++; + } + v.getTests().add(t); + } + if (sat) { + v.setResult("SAT"); + v.setComment("There is at least one path '"+ source + "' can use to reach '" + destination + + "'. See all the available paths below"); + + } + else if (unsat == tests.size()) { + v.setResult("UNSAT"); + v.setComment("There isn't any path '"+ source + "' can use to reach '" + destination + + "'. See all the checked paths below"); + + } + + return v; + } + + public List> getPaths(long graphId, String source, String destination) throws JsonParseException, JsonMappingException, JAXBException, IOException, MyInvalidDirectionException { + if (graphId < 0) { + throw new ForbiddenException("Illegal graph id: " + graphId); + } + GraphService graphService = new GraphService(); + Graph graph = graphService.getGraph(graphId); + if (graph == null) { + throw new DataNotFoundException("Graph with id " + graphId + " not found"); + } + + if (source == null || source.equals("")) { + throw new BadRequestException("Please specify the 'source' parameter in your request"); + } + if (destination == null || destination.equals("")) { + throw new BadRequestException("Please specify the 'destination' parameter in your request"); + } + + Node sourceNode = graph.searchNodeByName(source); + Node destinationNode = graph.searchNodeByName(destination); + + if (sourceNode == null) { + throw new BadRequestException("The 'source' parameter '" + source + "' is not valid, please insert the name of an existing node"); + } + if (destinationNode == null) { + throw new BadRequestException("The 'destination' parameter '" + destination + "' is not valid, please insert the name of an existing node"); + } + + Paths all_paths = getPaths(graph, sourceNode, destinationNode); + + if (all_paths.getPath().size() == 0) { + vlogger.logger.info("No path available"); + //System.out.println("No path available"); + return null; + } + + List> sanitizedPaths = sanitizePaths(all_paths); + + printListsOfStrings("Paths", sanitizedPaths); + + if (sanitizedPaths.isEmpty()) { + return null; + } + + List> paths=new ArrayList>(); + List p= new ArrayList(); + + for(int i=0; i name=sanitizedPaths.get(i); + for(int j=0; j