
18 Oct
2014
18 Oct
'14
1:07 a.m.
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