Hi, I have a project where I need to check some properties against a small UML model. I need the properties to be translated to Linear Temporal Logic to be used in a Java test suite. The properties are medical requirements (sentences), taken from a clinical guideline, and will be provided to you in English along with the model code. I need someone with knowledge in LTL, model checking, and software development, who can take a quick look at the code and choose the correct atomic propositions accordingly. If you need more information, I will be happy to provide you with it.
Example: If hasSymptoms is true, finally always the diagnosis will be modified to HRC, LRC, MRC or NoCancer. "(AP(hasSymptoms) ==> F AP(diagnos == NoCancer || (diagnos == HRC || (diagnos == MRC)) || (diagnos == LRC) || diagnos == CC)", true)
There are about 13 of these sentences. If I get the results I expect, I may ask you to collaborate again in the near future.