make & make install error: multiple definitions for "rank" and "scc_stack"

[sim365]

I installed LTSmin following the instructions here: https://github.com/utwente-fmt/Rabin-STTT/tree/master/mcc-experiments

Configuration seems to run smoothly, but I get errors running the last step with make & make install. It says that "rank" and "scc_stack" have multiple definitions. Am I doing something wrong or is it the object files? For reference, I'm attaching the result of ./configure and make & make install below

./configure --prefix=$HOME/install PKG_CONFIG_LIBDIR="$HOME/install/lib/pkgconfig" --without-sylvan --without-scoop Running the above yields this configuration:

make CFLAGS="-DCHECKER_TIMEOUT_TIME=600 -O2" && make install Running the above yields these errors:

[jacopol]

I have not seen this before, but "ltl2ba" is from SPOT. You will only need that dependency if you intend to do LTL model checking. I see you are also including OPAAL. At the moment, this only supports a subset of the full Uppaal language.

[sim365]

LTL model checking is the goal. In fact, I'm trying to replicate the Rabin-STTT experiments to a degree (the link at the top of the issue). It's strange that the files that seem to be erroring out haven't been updated in years, but no one has run into the issue I'm facing so far.

[jacopol]

OK, I see, so you checked out branch "-b spin2017" is that right? I cannot reproduce this here right now (already getting compilation errors from Spot).

couvreurnew.cc: In member function ‘spot::{anonymous}::couvreur99_new<is_explicit, strength>::check_result::operator bool() const’:
couvreurnew.cc:616:20: error: cannot convert ‘const emptiness_check_result_ptr’ {aka ‘const std::shared_ptr<spot::emptiness_check_result>’} to ‘bool’ in return
  616 |             return ecr;
      |                    ^~~
      |                    |
      |                    const emptiness_check_result_ptr {aka const std::shared_ptr<spot::emptiness_check_result>}

[sim365]

That is correct.

That's strange. I tried to start from scratch again, and I got no compilation errors. Which part of the installation in Rabin-STTT yields the error you're getting?

[jacopol]

I get this when installing Spot (make)

[jacopol]

Regarding your problem: Is it possible that current compilers are more strict than a few years ago? (regarding checking for multiple definitions).

[alaarman]

Yes, compilers definitely became more strict. But it sounds like the problem is resolved?

If not then I think a small edit in ltl2ba can fix it: In generalized.c change GScc scc_stack; to static GScc scc_stack;

[sim365]

@jacopol You're probably right on that. I've been seeing people use -fcommon as a bandaid to the problem

@alaarman The problem is, unfortunately, persistent. This is the result of make after changing from GScc to static:

[alaarman]

static GScc *scc_stack;