Commit f708873b authored by Simone Vuotto's avatar Simone Vuotto

Add Task entity, controller and service + Consistency Checking

parent a7a0df09
package it.unige.ReqV.engine;
import it.unige.ReqV.projects.tasks.Task;
import it.unige.ReqV.projects.tasks.TaskRepository;
import it.unige.ReqV.requirements.Requirement;
import rcc.ConsistencyChecker;
import rcc.InconsistencyFinder;
import rcc.mc.NuSMV;
import snl2fl.Snl2FlException;
import snl2fl.Snl2FlParser;
import snl2fl.ltl.nusmv.NuSMVTranslator;
import java.io.ByteArrayOutputStream;
import java.io.File;
import java.io.IOException;
import java.util.List;
import java.util.concurrent.atomic.AtomicInteger;
public class Snl2FlEngine implements ProjectEngine {
......@@ -38,6 +46,81 @@ public class Snl2FlEngine implements ProjectEngine {
} catch (Snl2FlException e) {
return null;
}
}
public void runConsistencyCheck(TaskRepository taskRepository, Task task, List<Requirement> reqList) {
try {
Snl2FlParser parser = new Snl2FlParser();
parseReqList(parser, reqList);
File tempFile = File.createTempFile("/tmp/out_" + task.getProject().getId(), ".nusmv");
ConsistencyChecker cc = new ConsistencyChecker(new NuSMV(300), parser, tempFile.getAbsolutePath());
final long taskId = task.getId();
cc.runAsync((res) -> {
Task runningTask = taskRepository.findOne(taskId);
if (res == ConsistencyChecker.Result.CONSISTENT)
runningTask.setStatus(Task.Status.SUCCESS);
else
runningTask.setStatus(Task.Status.FAIL);
runningTask.appendLog(cc.getMc().getMessage());
taskRepository.save(runningTask);
tempFile.delete();
});
} catch (Snl2FlException | IOException e) {
task.appendLog("[ERROR] " + e.getMessage());
}
}
public void runInconsistencyExplanation(TaskRepository taskRepository, Task task, List<Requirement> reqList) {
try {
Snl2FlParser parser = new Snl2FlParser();
parseReqList(parser, reqList);
File tempFile = File.createTempFile("/tmp/out_" + task.getProject().getId(), ".nusmv");
ConsistencyChecker cc = new ConsistencyChecker(new NuSMV(300), parser, tempFile.getAbsolutePath());
InconsistencyFinder inconsistencyFinder = new InconsistencyFinder(cc);
AtomicInteger counter = new AtomicInteger();
final long taskId = task.getId();
final int reqSize = reqList.size();
inconsistencyFinder.runAsync(
(requirement, result) -> {
Task runningTask = taskRepository.findOne(taskId);
if(result == ConsistencyChecker.Result.FAIL) {
runningTask.appendLog("[ERROR] Error occured during consistency check");
runningTask.setStatus(Task.Status.FAIL);
}
else
runningTask.appendLog(counter.incrementAndGet() + "/" + reqSize);
taskRepository.save(runningTask);
},
(inconsistentReqs) -> {
Task runningTask = taskRepository.findOne(taskId);
runningTask.appendLog("\n\n##################################################################");
runningTask.appendLog("Minimum Unsatisfiable core of " + inconsistentReqs.size() + " requirements found:");
for(snl2fl.req.requirements.Requirement r : inconsistentReqs)
runningTask.appendLog(r.getText());
runningTask.setStatus(Task.Status.SUCCESS);
taskRepository.save(runningTask);
tempFile.delete();
});
} catch (Snl2FlException | IOException e) {
task.appendLog("[ERROR] " + e.getMessage());
}
}
private void parseReqList(Snl2FlParser parser, List<Requirement> reqList) {
for (Requirement req : reqList) {
parser.parseString(req.getText());
}
}
}
package it.unige.ReqV.projects.tasks;
import com.fasterxml.jackson.annotation.*;
import it.unige.ReqV.projects.Project;
import javax.persistence.*;
import javax.validation.constraints.NotNull;
import java.util.Date;
@Entity
@JsonIgnoreProperties({"hibernateLazyInitializer", "handler"})
public class Task {
public enum Status {
SUCCESS,
FAIL,
RUNNING
}
public enum Type {
TRANSLATE,
CONSISTENCY_CHECKING,
MINIMUM_UNSATISFIABLE_CORE
}
@Id
@GeneratedValue(strategy = GenerationType.IDENTITY)
private Long id;
@NotNull
private String description;
@NotNull
@ManyToOne
@JsonIdentityInfo(generator = ObjectIdGenerators.PropertyGenerator.class, property = "id")
@JsonIdentityReference(alwaysAsId = true)
private Project project;
@NotNull
private Type type;
@NotNull
private Status status;
@NotNull
@JsonFormat(shape = JsonFormat.Shape.STRING, pattern = "dd-MM-yyyy hh:mm:ss")
@Temporal(TemporalType.TIMESTAMP)
private Date timestamp;
@Column(columnDefinition = "TEXT")
private String log;
public Task() { }
public Task(String description, Project project, Type type, Status status, Date timestamp, String log) {
this.description = description;
this.project = project;
this.type = type;
this.status = status;
this.timestamp = timestamp;
this.log = log;
}
public Task(String description, Project project, Type type) {
this.description = description;
this.project = project;
this.type = type;
this.status = Status.RUNNING;
this.timestamp = new Date();
this.log = "";
}
public Long getId() {
return id;
}
public void setId(Long id) {
this.id = id;
}
public String getDescription() {
return description;
}
public void setDescription(String description) {
this.description = description;
}
public Project getProject() {
return project;
}
public void setProject(Project project) {
this.project = project;
}
public Type getType() {
return type;
}
public void setType(Type type) {
this.type = type;
}
public Status getStatus() {
return status;
}
public void setStatus(Status status) {
this.status = status;
}
public Date getTimestamp() {
return timestamp;
}
public void setTimestamp(Date timestamp) {
this.timestamp = timestamp;
}
public String getLog() {
return log;
}
public void setLog(String log) {
this.log = log;
}
public void appendLog(String log) {
this.log += log + "\n";
}
@Override
public String toString() {
return "Task[id=" +id + ", pid=" + project.getId() + ", descrption='" + description + "', status=" + status + ", type=" + type + "]";
}
}
package it.unige.ReqV.projects.tasks;
import org.springframework.beans.factory.annotation.Autowired;
import org.springframework.http.HttpHeaders;
import org.springframework.http.HttpStatus;
import org.springframework.http.MediaType;
import org.springframework.http.ResponseEntity;
import org.springframework.web.bind.annotation.*;
import java.io.ByteArrayOutputStream;
import java.util.List;
@RestController
@RequestMapping("/projects/{pid}/tasks")
public class TaskController {
private TaskService taskService;
@Autowired
TaskController(TaskService taskService) {
this.taskService = taskService;
}
@GetMapping("")
public List<Task> getTasks(@PathVariable("pid") Long projectId) {
return taskService.getTasks(projectId);
}
@GetMapping("/{tid}")
public Task getTask(@PathVariable("pid") Long projectId, @PathVariable("tid") Long taskId) {
return taskService.getTask(projectId, taskId);
}
@GetMapping("/translate")
public ResponseEntity<?> translateRequirements(@PathVariable("pid") Long projectId) {
ByteArrayOutputStream stream = taskService.translate(projectId);
if(stream == null || stream.toByteArray().length == 0)
return new ResponseEntity<>("Impossible to translate, check that all requirements are compliant", HttpStatus.BAD_REQUEST);
HttpHeaders header = new HttpHeaders();
header.setContentType(MediaType.APPLICATION_OCTET_STREAM);
return new ResponseEntity<>(stream.toByteArray(), header, HttpStatus.OK);
}
@GetMapping("/consistencyCheck")
public Task consistencyCheck(@PathVariable("pid") Long projectId) {
return taskService.consistencyChecking(projectId);
}
@GetMapping("/findInconsistency")
public Task computeMuc(@PathVariable("pid") Long projectId) {
return taskService.computeMUC(projectId);
}
}
package it.unige.ReqV.projects.tasks;
import it.unige.ReqV.projects.Project;
import org.springframework.data.jpa.repository.JpaRepository;
import java.util.List;
public interface TaskRepository extends JpaRepository<Task, Long> {
List<Task> findByProjectOrderByIdDesc(Project project);
}
package it.unige.ReqV.projects.tasks;
import it.unige.ReqV.engine.EngineFactory;
import it.unige.ReqV.engine.Snl2FlEngine;
import it.unige.ReqV.projects.Project;
import it.unige.ReqV.projects.ProjectService;
import it.unige.ReqV.requirements.Requirement;
import it.unige.ReqV.requirements.RequirementService;
import org.springframework.beans.factory.annotation.Autowired;
import org.springframework.stereotype.Service;
import javax.persistence.EntityNotFoundException;
import java.io.ByteArrayOutputStream;
import java.util.List;
@Service
public class TaskService {
private ProjectService projectService;
private RequirementService requirementService;
private TaskRepository taskRepository;
@Autowired
public TaskService(ProjectService projectService,
RequirementService requirementService,
TaskRepository taskRepository) {
this.projectService = projectService;
this.requirementService = requirementService;
this.taskRepository = taskRepository;
}
public Task getTask(Long projectId, Long taskId) {
Project project = projectService.getProjectOfAuthUser(projectId);
Task task = taskRepository.getOne(taskId);
if(task == null || !task.getProject().getId().equals(project.getId()))
throw new EntityNotFoundException("Task with id " + taskId + " not found");
return task;
}
public List<Task> getTasks(Long projectId) {
Project project = projectService.getProjectOfAuthUser(projectId);
return taskRepository.findByProjectOrderByIdDesc(project);
}
public ByteArrayOutputStream translate(Long projectId) {
Project project = projectService.getProjectOfAuthUser(projectId);
List<Requirement> reqList = requirementService.getProjectRequirements(project);
if(reqList == null || reqList.isEmpty())
return null;
ByteArrayOutputStream stream = EngineFactory.getEngine(project.getType()).translate(reqList);
// TODO: save Task in db
return stream;
}
public Task consistencyChecking(Long projectId) {
Project project = projectService.getProjectOfAuthUser(projectId);
List<Requirement> reqList = requirementService.getProjectRequirements(project);
if(reqList == null || reqList.isEmpty())
return null;
String taskDescription = "Consistency checking " + reqList.size() + " requirements";
Task task = new Task(taskDescription, project, Task.Type.CONSISTENCY_CHECKING);
task = taskRepository.save(task);
Snl2FlEngine engine = new Snl2FlEngine();
engine.runConsistencyCheck(taskRepository, task, reqList);
return task;
}
public Task computeMUC(Long projectId) {
Project project = projectService.getProjectOfAuthUser(projectId);
List<Requirement> reqList = requirementService.getProjectRequirements(project);
if(reqList == null || reqList.isEmpty())
return null;
String taskDescription = "Computing Minimum Unsatisfiable Core of " + reqList.size() + " requirements";
Task task = new Task(taskDescription, project, Task.Type.MINIMUM_UNSATISFIABLE_CORE);
task = taskRepository.save(task);
Snl2FlEngine engine = new Snl2FlEngine();
engine.runInconsistencyExplanation(taskRepository, task, reqList);
return task;
}
}
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment