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
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
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
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
Hi,
the manual says in the section DESCRIPTION:
The list of automata to use should be supplied on standard input, or using
the -f or -F options.
However, the tool knows no -f option.
Fanda
I downloaded the spot tar package and tried to compile it using
./configure, make, sudo make install. However, make reports the error:
make: *** No targets specified and no makefile found. Stop.
and sudo make install reports:
make: *** No rule to make target 'install'. Stop.
What's happening, what can I do?
Thank you in advance,
-Pedro Marquez, Prof.
Hello,
I was trying to build Spot on a fresh ArchLinux install, when I came
across this issue:
> $ ./configure ...
> [...]
> checking for swig3.0... no
> checking for swig... no
> [...]
> $ make
> [...]
> swig -c++ -python -py3 -O -nofastproxy -MD -I../buddy/src -MF
> .deps/buddy_wrap.TPcxx ./buddy.i
> make[3]: swig: Command not found
> [...]
> make: *** [Makefile:1163: all] Error 2
If Spot requires Swig, shouldn't `configure` fail ? Or, if Swig is only
required for users who want to build the Python library, shouldn't the
latter not be included in the `all` rule ?
If that's any help, I attached my config.log.
Regards,
--
Clément 'Cigix' Gillard
"EAT SLEEP EAT REPEAT" @skrillbug_bot, 2016-06-23
