pstlab / oRatio

oRatio is an Integrated Logic and Constraint based solver
Apache License 2.0
6 stars 1 forks source link

Segmentation Fault when using multiple instances of a class, depending of the member's name #18

Closed Raffarti closed 3 years ago

Raffarti commented 4 years ago

This rddl is encourring in segmentation fault, but just renaming ctrl to rctrl does not. Some names works, others not. Commenting out r_at1 does also work.

class Waypoint {
    real id;

    Waypoint(real id) : id (id) { }
}

class RoverMotionSystem : StateVariable {
    Rover rover;
    RoverMotionSystem(Rover rover) : rover(rover) {}

    predicate At(Waypoint w) {
    }
}
class RoverController : StateVariable {
    Rover rover;
    RoverController(Rover rover) : rover(rover) {}
}
class Store : StateVariable {
    Rover rover;
    Store(Rover rover) : rover(rover) {}
}
class Rover {
    real id;
    RoverMotionSystem motion;
    RoverController ctrl;
    Store store;

    Rover(real id) : id(id), motion(new RoverMotionSystem(this)), ctrl(new RoverController(this)), store(new Store(this)) {}
}

Waypoint w0 = new Waypoint(0.0);
Waypoint w1 = new Waypoint(1.0);

Rover r = new Rover(0.0);
Rover r1 = new Rover(1.0);

fact r_at = new r.motion.At(w:w0, start:origin);
fact r_at1 = new r1.motion.At(w:w1, start:origin);

origin == 0.0;
riccardodebenedictis commented 4 years ago

This issue is related with the problem of checking the equality between two objects (in this case, the equality of the two facts and, more specifically, their tau variables).

Since objects might have fields, the equality of two objects might depend from the equality of their fields (deep equals), resulting in a tree of equality checks. This tree is currently visited in depth (recursive step at line 66):

https://github.com/pstlab/oRatio/blob/0ec136fc60240e6cf090c8a6ba5055f84a215ac1/core/item.cpp#L60-L72

leading, in some cases, to a stack overflow (r==r1 if r.ctrl==r1.ctrl if r.ctrl.rover==r1.ctrl.rover if r.ctrl.rover.ctrl==r1.ctrl.rover.ctrl, etc...).

This check has to be reimplemented so as to visit the tree in breadth.

Since object's fields are stored on a (ordered) map, a possible workaround is to name the fields in a way such that primitive objects (e.g., the Rover's id) appear, alphabetically, first.

riccardodebenedictis commented 4 years ago

currently, two instances are considered equal if their properties are equal. however, it is probably much simpler (and correct!) to consider two different objects just different, limiting deep equality check to the case of atoms.

Raffarti commented 4 years ago

consider two different objects just different

As in

Object o0 = new Object();
Object o1 = new Object();

would be considered different and no longer requiring an id field for instance?

riccardodebenedictis commented 4 years ago

Precisely!

way much simpler and no need of boilerplate ids..

thanks for pointing it out! :wink: