search

TAPAAL / verifytapn

VerifyTAPN is a stand-alone verification engine for timed-arc Petri nets, developed for the verification tool TAPAAL.
https://www.tapaal.net
GNU General Public License v2.0
1 stars 4 forks source link

Segfault when using inclusion check at certain token bound #28

Open ThomasMG opened 1 year ago

ThomasMG commented 1 year ago

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 commented 1 year ago

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