memory leak triggered by Context contents

Description

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

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 PM
Edited

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

Assignee

Reporter

Time tracking

10m logged

Priority

Created April 11, 2013 at 7:33 PM
Updated April 15, 2013 at 3:51 PM
Resolved April 12, 2013 at 3:24 PM