Hello,
I'm an undergraduate student at UBC working on a log analysis project
under Ivan
Beschastnikh <http://www.cs.ubc.ca/~bestchai/>. I'm using SPOT in the
project to parse LTL strings into formulae, and now trying to use the
translation to automata functionality.
The situation I'm dealing with would involve passing a finite sequence of
states into the automaton, and the description of the Monitor output
appeared to be what I needed. However, the monitor DFA provided for the
response formula G(a->Fb) was an all-accepting DFA:
which didn't seem to align with the given definition of monitor.
I've been searching the documentation, but can't find anything more
describing why this DFA would be produced. I've also been looking for a
description of acceptance condition syntax, especially for the state-based
degeneralized Buchi automaton, where both edges and states are labeled as
accepting.
Could you direct me to any documentation on these subjects or give any
insight on why the above monitor is being produced for the response
pattern? (As defined by the specification pattern project here
<http://patterns.projects.cis.ksu.edu/documentation/patterns/ltl.shtml>.)
Merci,
Caroline Lemieux
