and adjust it to detect siPSL formulas, as in the paper of Dax et
al. (ATVA'09). For issue #51.
* src/ltlast/atomic_prop.cc, src/ltlast/binop.cc,
src/ltlast/bunop.cc, src/ltlast/constant.cc, src/ltlast/formula.cc,
src/ltlast/formula.hh, src/ltlast/multop.cc, src/ltlast/unop.cc: Rename
the property, and adjust its computation on siSERE.
* src/ltlvisit/remove_x.cc, src/ltlvisit/simplify.cc,
src/tgbaalgos/stutter.cc: Adjust to new names.
* src/bin/ltlfilt.cc: Add option --syntactic-sutter-invariant.
* src/ltltest/kind.test: Update tests and add some new.
This operator is to ':' what [*i..j] is to ';'.
Part of issue #51.
* doc/tl/tl.tex: Document syntax, semantic, and trivial
simplifications.
* doc/tl/spotltl.sty: Add macros for new operators.
* src/ltlast/bunop.cc, src/ltlast/bunop.hh: Implement it.
* src/ltlast/multop.cc: Add some trivial simplifications.
* src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll: Parse it.
* src/ltltest/equals.test, src/ltltest/latex.test,
src/tgbatest/ltl2tgba.test: Add more tests.
* src/ltlvisit/randomltl.cc: Output this operator in
random PSL formulas.
* src/ltltest/rand.test: Adjust.
* src/tgbaalgos/ltl2tgba_fm.cc: Add translation rules.
* src/ltlvisit/tostring.cc: Add pretty printing code.
* src/ltlvisit/simplify.cc, src/ltlvisit/snf.cc: Adjust
switches.
* NEWS: Mention the new operator.
Fixes#50.
* src/tgbaalgos/cycles.cc, src/tgbaalgos/cycles.hh: Rewrite using
unsigned instead of state*, and std::vector instead of std::map.
* src/tgbaalgos/isweakscc.cc, src/tgbaalgos/powerset.cc: Adjust.
This helps issue #26 considerably, but I'm not closing it because there
are a few places here and there that can be cleaned up. For instance
build_state_set in minimize.cc should be rewritten.
* src/misc/bitvect.hh (bitvector_array::clear_all): New method.
* src/tgbaalgos/powerset.cc (tgba_powerset): Rewrite it.
* src/tgbaalgos/powerset.hh (power_map): Simplify.
Fixes#46.
* src/tgbaalgos/neverclaim.cc: Add option '6'.
* src/bin/common_aoutput.cc, src/bin/dstar2tgba.cc: Make it
possible to use the option.
* NEWS, doc/org/oaut.org: Document it.
* src/tgbatest/ltlcross2.test: Test it.
* src/sanity/style.test: Check for it.
* src/dstarparse/nra2nba.cc, src/dstarparse/nsa2tgba.cc,
src/tgbaalgos/randomize.cc, src/tgbaalgos/stutter.cc: Fix all those.
The namespace dstaryy was declared inline and then reopened as
non-inline. Likewise for hoayy. Let's use different names.
* src/dstarparse/dstarparse.yy, src/hoaparse/hoaparse.yy: Here.
* src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.hh: add
scc_info::begin() and scc_info::end() methods to iterate over the
node_ vector. Tidy the scc_node structure that that its member
are accessed via methods.
* src/tgbaalgos/safety.cc, src/bin/ltlcross.cc: Simplify using
this interface.
autfilt would segfault after reading any file, because the local result_
structure used in hoaparse has the same name as the local result_
structure used in dstarparse. For some reason I can only see this
problem using clang-3.5, not with gcc.
* src/dstarparse/dstarparse.yy, src/hoaparse/hoaparse.yy: Declare both
structures in a different namespace.
The dotty output changed to be horizontal, and also
the acceptance sets are now numbers.
* doc/org/dstar2tgba.org, doc/org/ltl2tgba.org, doc/org/ltl2tgta.org,
doc/org/satmin.org: Adjust these four.
Combined with 87c2b29, this fixes#7.
* src/tgbaalgos/stutterize.cc: Call keep_props().
* src/tgbaalgos/closure.cc: Just specify the encoding.
* src/bin/autfilt.cc: Add a --instut=2 option.
* src/tgbatest/stutter.test: More test.
* src/hoaparse/hoaparse.yy: validate deterministic and
complete when parsing HOA. Also set the deterministic
property on the TGBA.
* src/tgbatest/hoaparse.test: Test errors.
