First of all, you need to load nuMonitor.pl in SWI-Prolog.
To use the script exploiting syntactic encoding:
?- LTL = <your_LTL_formula>, monitor6(syntactic, LTL, <Alphabet>, <Trace>, Verdict).To use the script exploiting semantic encoding:
?- LTL = <your_LTL_formula>, monitor6(semantic, LTL, <Alphabet>, <Trace>, Verdict).The Verdict variable is unified with the monitor's verdict.
?- LTL = eventually(prop(p,tt)), monitor6(syntactic, LTL, [p,q,s], [[q], [q,s]], Verdict).Expected result: Verdict = ?(tt)
?- LTL = eventually(prop(p,tt)), monitor6(semantic, LTL, [p,q,s], [[q], [q,s]], Verdict).Expected result: Verdict = ?(tt)
?- LTL = eventually(prop(p,tt)), monitor6(syntactic, LTL, [p,q,s], [[q], [q,s], [p]], Verdict).Expected result: Verdict = tt
?- LTL = eventually(prop(p,tt)), monitor6(semantic, LTL, [p,q,s], [[q], [q,s], [p]], Verdict).Expected result: Verdict = tt
?- LTL = globally(prop(p,tt)), monitor6(syntactic, LTL, [p,q,s], [[p,q], [p]], Verdict).Expected result: Verdict = ?(ff)
?- LTL = globally(prop(p,tt)), monitor6(semantic, LTL, [p,q,s], [[p,q], [p]], Verdict).Expected result: Verdict = ?(ff)
?- LTL = globally(prop(p,tt)), monitor6(syntactic, LTL, [p,q,s], [[p,q], [p], [q]], Verdict).Expected result: Verdict = ff
?- LTL = globally(prop(p,tt)), monitor6(semantic, LTL, [p,q,s], [[p,q], [p], [q]], Verdict).Expected result: Verdict = ff
?- LTL = globally(eventually(prop(p,tt))), monitor6(syntactic, LTL, [p,q,s], [[p,q], [p], [q]], Verdict).Expected result: Verdict = x
?- LTL = globally(eventually(prop(p,tt))), monitor6(semantic, LTL, [p,q,s], [[p,q], [p], [q]], Verdict).Expected result: Verdict = x
Counterexample showing that Syntactic encoding is not the best approximation (this causes the syntactic monitor to lose anticipation)
?- LTL = until(prop(p,tt), ff), monitor6(syntactic, LTL, [p,q,s], [[p]], Verdict).Expected result: Verdict = ?(ff)
?- LTL = until(prop(p,tt), ff), monitor6(semantic, LTL, [p,q,s], [[p]], Verdict).Expected result: Verdict = ff