Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
sim365 opened this issue Jun 22, 2023 · 9 comments
Open

Comments

@sim365
Copy link

sim365 commented Jun 22, 2023

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:
image

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

@jacopol
Copy link
Contributor

jacopol commented Jun 22, 2023

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
Copy link
Author

sim365 commented Jun 22, 2023

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
Copy link
Contributor

jacopol commented Jun 22, 2023

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
Copy link
Author

sim365 commented Jun 23, 2023

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
Copy link
Contributor

jacopol commented Jun 23, 2023

I get this when installing Spot (make)

@jacopol
Copy link
Contributor

jacopol commented Jun 23, 2023

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

@alaarman
Copy link
Collaborator

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
Copy link
Author

sim365 commented Jun 23, 2023

@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:
image

@alaarman
Copy link
Collaborator

static GScc *scc_stack;

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants