meyerphi / strix Goto Github PK
View Code? Open in Web Editor NEWStrix is a tool for reactive synthesis of controllers from LTL specifications.
License: GNU Affero General Public License v3.0
Strix is a tool for reactive synthesis of controllers from LTL specifications.
License: GNU Affero General Public License v3.0
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
Online Demo does not seem to provide the display of the synthesized mealy machine anymore.
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!
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
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.