meyerphi/strix

Strix is a tool for reactive synthesis of controllers from LTL specifications.

Strix

Strix is a tool for reactive synthesis of controllers from LTL specifications.

To build Strix from source, see the build instructions. For details on how to use Strix, see the usage instructions. The supported input and output formats are given in the formats description.

Strix is licensed under the AGPLv3, for details see LICENSE.md. It includes code from several authors with partially different licenses, for a list see AUTHORS.md.

Older releases of Strix can be found on the old homepage. The previous source code can be found on the old GitLab repository.

strix's Issues

Support for KISS format

Are there any plans to add back support for KISS output? This was a breaking change for me and I am hoping to not have to rewrite my code. Or do you know of any tools that would convert HOAF to KISS?

Thanks for making such an awesome tool!

Parsing error

Seems like strix has trouble understanding variables starting with capital letters. (The docs say it supports such though.)

$ ~/software/strix/strix -f 'G (r -> F g) && F NoHigh' --ins r
line 1:18 no viable alternative at input 'FN'
org.antlr.v4.runtime.misc.ParseCancellationException
	at org.antlr.v4.runtime.BailErrorStrategy.recover(BailErrorStrategy.java:51)
	at owl.grammar.LTLParser.binaryExpression(LTLParser.java:424)
	at owl.grammar.LTLParser.andExpression(LTLParser.java:313)
	at owl.grammar.LTLParser.orExpression(LTLParser.java:235)
	at owl.grammar.LTLParser.expression(LTLParser.java:183)
	at owl.grammar.LTLParser.formula(LTLParser.java:136)
	at owl.ltl.parser.LtlParser.parse(LtlParser.java:59)
	at owl.cinterface.CLabelledFormula.parse(CLabelledFormula.java:82)
Caused by: org.antlr.v4.runtime.NoViableAltException
	at org.antlr.v4.runtime.atn.ParserATNSimulator.noViableAlt(ParserATNSimulator.java:2026)
	at org.antlr.v4.runtime.atn.ParserATNSimulator.execATN(ParserATNSimulator.java:467)
	at org.antlr.v4.runtime.atn.ParserATNSimulator.adaptivePredict(ParserATNSimulator.java:393)
	at owl.grammar.LTLParser.binaryExpression(LTLParser.java:398)
	... 6 more

Version: strix 21.0.0

Online Demo Not Working

Online Demo does not seem to provide the display of the synthesized mealy machine anymore.

Assertion failure in ZLK solver

Description:
When trying to run Strix with the following configuration: solver=ZLK exploration=BSF output=aag, which is the winning configuration in the SYNTCOMP).
The assertion assert!(!compute_strategy) in the file zlk.rs fails.

Produce Steps:
Example of CLI running (Benchmark ltl2dpa04):

strix -f "((G ((p0) <-> (! (p1)))) && ((F ((a) && (b))) <-> (G (F (p0)))))" --ins="b,a" --outs="p1,p0" -o aag -e bfs --solver zlk

Output (with RUST_BACKTRACE=full):

thread 'main' panicked at 'assertion failed: !compute_strategy', src/parity/solver/zlk.rs:88:9
stack backtrace:
   0:     0x55f59c464bcd - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h941ee1421d11073a
   1:     0x55f59c4244be - core::fmt::write::h2f422cb945c805a2
   2:     0x55f59c44ef54 - std::io::Write::write_fmt::h8f9d0365ac9506ac
   3:     0x55f59c451c24 - std::panicking::default_hook::{{closure}}::hbe1e3ca4f89cf8c0
   4:     0x55f59c4524a9 - std::panicking::rust_panic_with_hook::he1ec1558452e9d0b
   5:     0x55f59c464fab - std::panicking::begin_panic_handler::{{closure}}::h649428e396ec4455
   6:     0x55f59c464f46 - std::sys_common::backtrace::__rust_end_short_backtrace::h93616e22db15c924
   7:     0x55f59c451e52 - rust_begin_unwind
   8:     0x55f59c3bdce2 - core::panicking::panic_fmt::hd4a6277baa7a1fdc
   9:     0x55f59c3bdcac - core::panicking::panic::h0f4d8ccc452c22f3
  10:     0x55f59c480d35 - <strix::parity::solver::incremental::IncrementalSolver<S> as strix::parity::solver::incremental::IncrementalParityGameSolver>::strategy::h3cd37be1d6b602af
  11:     0x55f59c46f795 - strix::synthesize_with::he068b0e33b706938
  12:     0x55f59c3d5744 - strix::main::h64dfa4b5a95bd6a9
  13:     0x55f59c3d9d73 - std::sys_common::backtrace::__rust_begin_short_backtrace::he65005995cea8b77
  14:     0x55f59c3dd224 - main
  15:     0x7f413c9d9d85 - __libc_start_main
  16:     0x55f59c3c923e - _start
  17:                0x0 - <unknown>

Environment:
Strix version: Built from commit c0b1298 (The latest commit)
Rust Version: 1.60.0
OS: Rocky Linux 8.6