Hello,
My name is Dennis Park and I'm a student at the University of British
Columbia. I am using the Spot library in a research project I am currently
working on and I wanted to ask whether the Spot library supports negation
propagation.
More specifically, I would like to take an ltl formula
spot::ltl::formula* f
and propagate all negations in f so that negations only occur before atomic
propositions. Does the Spot library support such a functionality? If so,
where in the documentation could I find information on it (I tried to look
for something like it in the documentation but had trouble finding
anything).
Thank you,
Dennis Park
