Spot

Hi all, I am using SPOT by following command autfilt --equivalent-to=A.hoa B.hoa to check the equivalence of two Buchi automata A.hoa and B.hoa (attached). It returns nothing and it means two automata are not equivalent. But actually I used GOAL and RABIT to check the equivalence, they said yes. I think you may want to have a look. Regards, Yong -- Yong Li (李勇), State Key Lab. of Computer Science Institute of Software, Chinese Academy of Sciences

7 years, 5 months

Bug in ltlcross manual

by František Blahoudek

Hi, I think there is a bug in the manual of ltlcross. There is the paragraph > If the translator produced a Streett or Rabin automaton, these columns > contains the size of a TGBA (or BA) produced by ltlcross from that > Streett or Rabin automaton. Check in_states, in_edges, in_transitions, and in_acc for statistics about the actual input automaton. which seems no longer to be valid as I have no such columns in the output files created by ltlcross v. 2.4.4. Best, Fanda Blahoudek

7 years, 6 months

genaut --ks-nca error

by Florian Barta

Hi, when using genaut --ks-nca e.g. genaut --ks-nca=1..10 I get the following error: genaut: print_hoa(): automaton is complete but prop_complete()==false Is this a bug? What can I do to get the desired result? I am using spot version 2.4.1 on Ubuntu 16.04. Best regards, Florian Barta

7 years, 8 months

is_tt and is_ff in Python bindings

by František Blahoudek

Hi, I have found out that is_tt and is_ff does nt work as expected in Python. See the attached notebook for details. Best, Fanda Blahoudek

7 years, 8 months

genaut - documentation

by František Blahoudek

Hi, there is a tiny inconsistency in man genaut. For the families from Löding's paper there is ... 4N states ... less than n! states. I guess the n and N should share their case. Best, Fanda

7 years, 9 months

← Newer
1
...
13
14
15
16
17
18
19
...
22
Older →

Jump to page:

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Spot