summaryrefslogtreecommitdiffstats
path: root/verigraph/src/it/polito/verigraph/service
diff options
context:
space:
mode:
Diffstat (limited to 'verigraph/src/it/polito/verigraph/service')
-rw-r--r--verigraph/src/it/polito/verigraph/service/GraphService.java82
-rw-r--r--verigraph/src/it/polito/verigraph/service/JsonValidationService.java132
-rw-r--r--verigraph/src/it/polito/verigraph/service/NeighbourService.java143
-rw-r--r--verigraph/src/it/polito/verigraph/service/NodeService.java223
-rw-r--r--verigraph/src/it/polito/verigraph/service/ValidationUtils.java131
-rw-r--r--verigraph/src/it/polito/verigraph/service/VerificationService.java625
-rw-r--r--verigraph/src/it/polito/verigraph/service/VerigraphLogger.java71
7 files changed, 1407 insertions, 0 deletions
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<Graph> getAllGraphs() throws JsonProcessingException, MyNotFoundException {
+ List<Graph> 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<Entry<String, JsonNode>> iter = node.fields();
+ while (iter.hasNext()) {
+ Entry<String, JsonNode> 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<Neighbour> 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<Long, Neighbour> neighbours = manager.getNeighbours(graphId, nodeId);
+ return new ArrayList<Neighbour>(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<Node> 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<Long, Node> nodes =manager.getNodes(graphId);
+ return new ArrayList<Node>(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<Long, Node> 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<Long, Neighbour> 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<List<String>> sanitizePaths(Paths paths) {
+ List<List<String>> sanitizedPaths = new ArrayList<List<String>>();
+ for (String path : paths.getPath()) {
+ List<String> newPath = extractPath(path);
+ sanitizedPaths.add(newPath);
+ }
+ return sanitizedPaths;
+ }
+
+ private List<String> extractPath(String path) {
+ List<String> newPath = new ArrayList<String>();
+ // 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<List<String>> lists) {
+ vlogger.logger.info(message);
+ for (List<String> 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<List<String>> sanitizedPaths = sanitizePaths(paths);
+ List<Test> 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<Integer, GeneratorSolver> 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<Test> extractTestsFromPaths(Graph graph, List<List<String>> paths, String result) {
+ List<Test> tests = new ArrayList<Test>();
+ for (List<String> path : paths) {
+ List<Node> nodes = new ArrayList<Node>();
+ for (String nodeName : path) {
+ nodes.add(graph.searchNodeByName(nodeName));
+ }
+ tests.add(new Test(nodes, result));
+ }
+ return tests;
+ }
+
+ private Verification evaluateIsolationResults(List<Test> 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<List<String>> sanitizedPaths, String middleboxName) {
+ List<List<String>> pathsToBeRemoved = new ArrayList<List<String>>();
+ for (List<String> path : sanitizedPaths) {
+ boolean middleboxFound = false;
+ for (String node : path) {
+ if (node.equals(middleboxName)) {
+ middleboxFound = true;
+ break;
+ }
+ }
+ if (!middleboxFound) {
+ pathsToBeRemoved.add(path);
+ }
+ }
+ for (List<String> path : pathsToBeRemoved) {
+ sanitizedPaths.remove(path);
+ }
+
+ }
+
+ private void extractPathsWithoutMiddlebox(List<List<String>> sanitizedPaths, String middleboxName) {
+ List<List<String>> pathsToBeRemoved = new ArrayList<List<String>>();
+ for (List<String> path : sanitizedPaths) {
+ boolean middleboxFound = false;
+ for (String node : path) {
+ if (node.equals(middleboxName)) {
+ middleboxFound = true;
+ break;
+ }
+ }
+ if (middleboxFound) {
+ pathsToBeRemoved.add(path);
+ }
+ }
+ for (List<String> 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<List<String>> 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<Test> tests = extractTestsFromPaths(graph, pathsBetweenSourceAndDestination, "UNKNOWN");
+
+ List<List<String>> pathsWithMiddlebox = new ArrayList<List<String>>();
+ for (List<String> 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<Integer, GeneratorSolver> 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<Integer, GeneratorSolver> 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<Test> 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<List<String>> 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<Integer, GeneratorSolver> scenarios=createScenarios(sanitizedPaths, graph);
+
+ List<Test> 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<Test> run(Graph graph, Map<Integer, GeneratorSolver> scenarios, String src, String dst) {
+ List<Test> tests = new ArrayList<Test>();
+ String result;
+
+ //estimation time
+ //Long time=(long) 0;
+ //Calendar cal = Calendar.getInstance();
+ //Date start_time = cal.getTime();
+
+ for(Map.Entry<Integer, GeneratorSolver> t : scenarios.entrySet()){
+
+ result=t.getValue().run(src, dst);
+
+ List<Node> path = new ArrayList<Node>();
+ 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<Integer, GeneratorSolver> createScenarios(List<List<String>> sanitizedPaths, Graph graph) {
+ int index=0;
+ Map<Integer, GeneratorSolver> scenarios=new HashMap<Integer, GeneratorSolver>();
+ for(List<String> 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<Test> 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<List<Node>> 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<List<String>> sanitizedPaths = sanitizePaths(all_paths);
+
+ printListsOfStrings("Paths", sanitizedPaths);
+
+ if (sanitizedPaths.isEmpty()) {
+ return null;
+ }
+
+ List<List<Node>> paths=new ArrayList<List<Node>>();
+ List<Node> p= new ArrayList<Node>();
+
+ for(int i=0; i<sanitizedPaths.size(); i++){
+ List<String> name=sanitizedPaths.get(i);
+ for(int j=0; j<name.size(); j++){
+ Node n=graph.searchNodeByName(name.get(j));
+ if(n!=null)
+ p.add(j, n);
+ }
+ if(!p.isEmpty())
+ paths.add(i, p);
+ }
+
+ if(!paths.isEmpty())
+ return paths;
+ else
+ return null;
+ }
+} \ No newline at end of file
diff --git a/verigraph/src/it/polito/verigraph/service/VerigraphLogger.java b/verigraph/src/it/polito/verigraph/service/VerigraphLogger.java
new file mode 100644
index 0000000..b819538
--- /dev/null
+++ b/verigraph/src/it/polito/verigraph/service/VerigraphLogger.java
@@ -0,0 +1,71 @@
+/*******************************************************************************
+ * 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.logging.ConsoleHandler;
+import java.util.logging.FileHandler;
+import java.util.logging.Formatter;
+import java.util.logging.Handler;
+import java.util.logging.Level;
+import java.util.logging.LogManager;
+import java.util.logging.Logger;
+import java.util.logging.SimpleFormatter;
+
+public class VerigraphLogger {
+ static private FileHandler fileTxt;
+ static private SimpleFormatter formatterTxt;
+ private static VerigraphLogger verigraphlogger= new VerigraphLogger();
+ public static Logger logger;
+
+ private VerigraphLogger() {
+
+ // suppress the logging output to the console
+ /*Logger rootLogger = Logger.getLogger("");
+ Handler[] handlers = rootLogger.getHandlers();
+ if (handlers[0] instanceof ConsoleHandler) {
+ rootLogger.removeHandler(handlers[0]);
+ }*/
+
+ /*Logger globalLogger = Logger.getLogger("");
+ Handler[] handlers = globalLogger.getHandlers();
+ for(Handler handler : handlers) {
+ globalLogger.removeHandler(handler);
+ }*/
+
+ LogManager.getLogManager().reset();
+ // get the global logger to configure it
+ logger = Logger.getLogger(VerigraphLogger.class.getName());
+ // logger.setUseParentHandlers(false);
+ logger.setLevel(Level.INFO);
+ try {
+ if(System.getProperty("catalina.home") != null)
+ fileTxt = new FileHandler(System.getProperty("catalina.home")+"/logs/verigraph_log.txt");
+ else fileTxt= new FileHandler("verigraph_log.txt");
+
+ } catch (SecurityException e) {
+ // TODO Auto-generated catch block
+ e.printStackTrace();
+ } catch (IOException e) {
+ // TODO Auto-generated catch block
+ e.printStackTrace();
+ }
+
+ // create a TXT formatter
+ formatterTxt = new SimpleFormatter();
+ fileTxt.setFormatter(formatterTxt);
+ logger.addHandler(fileTxt);
+
+ }
+
+ public static VerigraphLogger getVerigraphlogger(){
+ return verigraphlogger;
+ }
+
+} \ No newline at end of file