Description
We analyzed the mission specifications contained in the Spectra examples collected in Exp2. We collected 1216 distinct LTL mission specifications and we analyzed each of these specifications. We verified whether it is possible to obtain the mission specifications starting from the patterns, by performing the following steps.
- For each property we automatically checked whether it was an instance of a mission specification pattern or a simple combination of mission specification patterns.
- We considered the properties that did not match any of the proposed patterns.
- We considered expressed using past temporal operators and we designed mission specifications for them.
Reproduction Kit
To extract mission specifications and get results in missionSpecificationExp3.txt, run
ExtractingSpecifications/exp3ExtrctMissionSpec.sh
To run Step1 (parsing errors on the console they are caused by non matching patterns):
Step1/java -jar Exp3.jar missionSpecificationExp3.txt
To run Step2 (parsing errors on the console they are caused by non matching patterns)
Step1/java -jar Exp3.jar missionSpecificationExp3.txt
To run Step3:
Step3/java -jar Exp3.jar input.txt
Specifications & Data
| Archive | File Contents # |
|---|---|
| Step1.zip | 13 |
| Step2.zip | 14 |
| Step3.zip | 13 |
| ExtractingSpecifications.zip | 10 |