Good morning all, creator here- I made this demo for you to explore a requirements engineering technique. Defects in the requirements engineering process have outsized cost in the overall product development cycle, especially in safety critical applications. Adding just a dash of formal methods in authoring tools can catch defects as they are introduced and provide timely feedback to engineers. This is a quick example of how to use a context-free grammar and an SMT solver (Z3 in this case) to automatically find logical contradictions, redundant conditions and inconsistency of entity names. Enjoy!

I like the visual output for the prepopulated examples, but I tried to interact with it myself by making up this string:

> If payload = bad, server shall email someone on blue team.

and I get this error:

> Error at position 32 ("load")

One improvement might be making this error message more clear. Character 32 is around "shall", but the quoted word is near the beginning of the text. I tried changing "payload" to "var" and "=" to "==" and I'm just getting less and less helpful errors before giving up.

Seems pretty cool but what the heck is the syntax?

"User shall send login message to server"

seems almost exactly like

"Server shall send req_resolution to ctrl_entity"

yet the former throws an unhelpful error. Your parser might want to just internally slap a `_` between unexpected tokens and try reparsing. Humans tend to use spaces between things.