memory leak triggered by Context contents
Description
Environment
Rodin 2.7,
OSX 10.8.3
ProB for Rodin 2.3.5
Attachments
2
Gliffy Diagrams
Activity
Show:
Jens Bendisposto April 15, 2013 at 3:51 PM
and are fixed in release ProB for Rodin 2.4.0
GintautasS April 12, 2013 at 4:30 PM
A very clear explanation. Thank you!
Michael Leuschel April 12, 2013 at 4:07 PMEdited
partition(SET,{A},{B},{A,B})
is by definition equivalent to:
SET = {A} \/ {B} \/ {A,B} & {A} /\ {B} = {} &
{A} /\ {A,B} = {} &
{B} /\ {A,B} = {}
The latter two conjuncts are false, so "partition(SET,...)" is equivalent to false, which ProB now detects.
(Sorry the wiki renders the text very strangely)
GintautasS April 12, 2013 at 4:02 PM
Does this work properly as a solution in ProB?
I mean is set {A, B} treated as a SET element like {A} or {B}?
constants A B
sets SET
axioms
@axm1 partition(SET, {A}, {B}, {A, B}
Michael Leuschel April 12, 2013 at 3:23 PM
Has just been fixed (commit 07dcdfbc92bb7d4c3384f95a17765005eed9ab2c).
It was a loop in the code detecting enumerated sets.
Fixed
Details
Details
Assignee
Michael LeuschelReporter
GintautasSTime tracking
10m logged
Priority
MinorCreated April 11, 2013 at 7:33 PM
Updated April 15, 2013 at 3:51 PM
Resolved April 12, 2013 at 3:24 PM
Hello,
although it may make no sense, but this bit "{A, B}" causes a sudden and nasty memory leak. If Rodin is not killed in time, that leak crashes the system.
Context
constants A B
sets SET
axioms
@axm1 partition(SET, {A}, {B}, {A, B})
How to reproduce the error:
1. import given project
2. start ProB animation/model checking
3. expect immediate memory leak in chunks of >300MB
Expected behaviour:
Error message or animation
Regards,
Gintautas