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

Segfault when using inclusion check at certain token bound #28

Open
ThomasMG opened this issue Aug 9, 2023 · 1 comment
Open

Segfault when using inclusion check at certain token bound #28

ThomasMG opened this issue Aug 9, 2023 · 1 comment

Comments

@ThomasMG
Copy link

ThomasMG commented Aug 9, 2023

I get an error when checking the query for the TAPN "alternating-bit-protocol" example net.
The error only seem to occur when the token bound is above 16 and inclusion check is enabled.

I execute the following:
./verifytapn --k-bound 16 --search-strategy MAX-COVER --inclusion-check 1 --inclusion-places *NONE* alternating-bit-protocol.xml alternating-bit-protocol.q

Linux

On Linux I always get the following output immediately:

Missing query-indexes for query-file (which is identified as XML-format), assuming only first query is to be verified
Using Maximum Cover Search
k-bound is: 16
Generating no trace
Symmetry Reduction is ON
Untimed place optimization is ON
Using local maximum constants for extrapolation
Using discrete inclusion marking factory
Considering the places  for discrete inclusion.
Model file is: ../build/verifytapn/bin/alternating-bit-protocol.xml
Query file is: ../build/verifytapn/bin/alternating-bit-protocol.q

Segmentation fault (core dumped)

Mac

The same does not happen on mac. Here it will execute the query and only occasionally give this output:

Missing query-indexes for query-file (which is identified as XML-format), assuming only first query is to be verified
Using Maximum Cover Search
k-bound is: 16
Generating no trace
Symmetry Reduction is ON
Untimed place optimization is ON
Using local maximum constants for extrapolation
Using discrete inclusion marking factory
Considering the places  for discrete inclusion.
Model file is: alternating-bit-protocol.xml
Query file is: alternating-bit-protocol.q


STATS
  discovered markings:  1078430
  explored markings:    83864
  stored markings:  49553


TRANSITION STATISTICS
<Protocol_Ack_rec_0:3436> <Protocol_Send_1:2380> <Protocol_Ack_send_0:3450> <Protocol_Loss_C:72415> <Protocol_Loss_D:59111> <Protocol_ReSend_1:48603>
<Protocol_Receive_old_1:2990> <Protocol_Ack_send_1:4889> <Protocol_Ack_rec_1:4849> <Protocol_Send_0:2380> <Protocol_Receive_0:5526> <Protocol_ReSend_0:22162>
<Protocol_Receive_old_0:3186> <Protocol_Loss_A:58857> <Protocol_Loss_B:57683> <Protocol_Receive_1:15987>

Query is NOT satisfied.
Max number of tokens found in any reachable marking: >16
verifytapn-osx64(73200,0x1140a4600) malloc: *** error for object 0x6000013ec400: pointer being freed was not allocated
verifytapn-osx64(73200,0x1140a4600) malloc: *** set a breakpoint in malloc_error_break to debug
Abort trap: 6
@srba
Copy link
Member

srba commented Aug 9, 2023

@ThomasMG , could you append the model and query file to this bug report please?

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

2 participants