Skip to content

syntcomp 2024.1

Choose a tag to compare

View all tags
@5nizza 5nizza released this 26 Oct 09:15
· 3 commits to master since this release
v2024.1
55194fe

Changes since last version:

  • SPOT version bumped to 2.12
  • Other libraries are also set to the latest versions
  • After translating UCW -> kUCW, call merge_states and merge_edges until converging. This reduces the kUCW size, and seem to speed up things, though there are examples where it makes things slower despite smaller kUCW.
  • Removed optimisation 'fix the local BDD order if it appears many times in final orders': this does not seem (?) to affect the performance, but it complicates the code.
  • Static linking by default (because it is then simpler to upload to StarExec for SyntComp).
  • Changed the semantics of -k parameter (also fixed the bug #4): now -k 4 -k 8 -k 12 means try all three values in order.
  • For small specs, the reachability-analysis optimisation is used when determinising strategies
  • For starexec server, there is a variant with ABC postprocessing of the resulting models (using a single dc2 command).

The binaries were compiled for x84_64 on Ubuntu 22.04.1 with gcc 11.4.0 with optimizations enabled.
The SPOT was compiled with the number of accepting sets increased from default 32 to 128.
The archive sdf-starexec.zip contains archives prepared for uploading to StarExec for SyntComp'24.

Full Changelog: https://github.com/5nizza/sdf-hoa/commits/v2024.1

Assets 3
Loading