We generated the LTL specifications of the considered mission requirements. We (i) negated the LTL specification; (ii) encoded the specification and the model of the scenario in NuSMV; (iii) used NuSMV to check whether the models contained a path that satisfied the mission specification (violates its negation). If a plan was present we used Simbad to simulate the robot executing the plan. We verified whether the results where correct: when we expected a plan to not be present in the given model, NuSMV was not able to compute it, and, when a plan was expected to be present it was computed by NuSMV. We also checked the correctness of the generated plans using the Simbad simulator.
To replicate this experiment run java -jar Exp4.jar randomMissions.txt 6 ./ true
Specifications & Data
|Archive||File Contents #|