Conversion from requirements to LTL

[amarbanerjee23]

Hi Team,
Is there any support to generate the LTL formula from the Requirements Language.
I tried to find the link but it turned out to be unsuccessful.
Request help if possible.
Cheers,
Amar

[SimoV8]

Hi Amar,

I've just updated the repository with the latest commits (you can see the most updated repository here).

Regarding your question, you can take a look at the tutorial in docs/TUTORIAL.md in this repository and follow the steps to parse and translate requirements.

I hope it helps :)
Cheers,
Simone

[amarbanerjee23]

Hi Simone,
I have been able to compile the source.
During the conversion of the input requirement "inconsistency1.req" to LTL, there seems to be a parsing error.

Exception in thread "main" it.sagelab.specpro.fe.ParseException at it.sagelab.specpro.fe.AbstractLTLFrontEnd.parse(AbstractLTLFrontEnd.java:73) at it.sagelab.specpro.fe.AbstractLTLFrontEnd.parseFile(AbstractLTLFrontEnd.java:30) at com.mncml.ltl.requirements2ltl.Requirements2LTL.requirements2LTL(Requirements2LTL.java:54) at com.mncml.ltl.requirements2ltl.Requirements2LTL.main(Requirements2LTL.java:140) **Caused by: org.antlr.v4.runtime.misc.ParseCancellationException: line 1:34 token recognition error at: '.'** at it.sagelab.specpro.fe.psp.parser.ThrowingErrorListener.syntaxError(ThrowingErrorListener.java:15) at org.antlr.v4.runtime.ProxyErrorListener.syntaxError(ProxyErrorListener.java:41) at org.antlr.v4.runtime.Lexer.notifyListeners(Lexer.java:364) at org.antlr.v4.runtime.Lexer.nextToken(Lexer.java:144) at org.antlr.v4.runtime.BufferedTokenStream.fetch(BufferedTokenStream.java:169) at org.antlr.v4.runtime.BufferedTokenStream.sync(BufferedTokenStream.java:152) at org.antlr.v4.runtime.BufferedTokenStream.consume(BufferedTokenStream.java:136) at org.antlr.v4.runtime.Parser.consume(Parser.java:571) at org.antlr.v4.runtime.Parser.match(Parser.java:203) at it.sagelab.specpro.fe.ltl.parser.LTLGrammarParser.formula(LTLGrammarParser.java:431) at it.sagelab.specpro.fe.ltl.parser.LTLGrammarParser.file(LTLGrammarParser.java:157) at it.sagelab.specpro.fe.LTLFrontEnd.getParseTree(LTLFrontEnd.java:30) at it.sagelab.specpro.fe.AbstractLTLFrontEnd.parse(AbstractLTLFrontEnd.java:69) ... 3 more
Can you please suggest any help ??
I had some more queries

1. Is there any available API to serialise the LTL model into an LTL file ?
2. Does spec-pro support LTL to Controller Synthesis ?
3. Any mechanism to convert LTL to KISS format ?

Cheers,
Amar