Projet_mcp_5

class Rectangle
{

  //*************************************************************************
  //FIELDS
  //*************************************************************************

  var startX: int;
  var startY: int;
  var endX: int;
  var endY: int;
  var value: int;

  //*************************************************************************
  //CLASS INVARIANTS
  //*************************************************************************

  predicate valid()
  reads this
  {
     0 <= startX < endX && 0 <= startY < endY && (value == 0 || value == 1)
  }

  constructor(sX: int, sY: int, eX: int, eY: int, v: int)
  requires 0 <= sX < eX
  requires 0 <= sY < eY
  requires ( v == 0 || v == 1)
  ensures valid()
  modifies this
  {
      startX := sX;
      startY := sY;
      endX := eX;
      endY := eY;
      value := v;
  }

  function method getStartX(): int
  reads this
  {
      startX
  }

  function method getStartY(): int
  reads this
  {
      startY
  }

  function method getEndX(): int
  reads this
  {
      endX
  }

  function method getEndY(): int
  reads this
  {
      endY
  }

  function method getValue(): int
  reads this
  {
      value
  }
}

class Couverture
{

    //*************************************************************************
    //FIELDS
    //*************************************************************************

    var couverture: array2<int>;
    var rectangles: seq<Rectangle>

    //*************************************************************************
    //CLASS INVARIANTS
    //*************************************************************************

    predicate valid()
    reads this, couverture, rectangles
    {
        couverture != null
        && couverture.Length0 > 0
        && couverture.Length1 > 0
        //&& |rectangles| > 0
        //&& forall i | 0 <= i < |rectangles| :: rectangles[i] != null
        //&& forall i | 0 <= i < |rectangles| :: rectangles[i].getStartX() <= couverture.Length0 && rectangles[i].getStartY() <= couverture.Length1
    }

    constructor(recList: seq<Rectangle>)

    // Il y a au moins un rectangle dans la list et aucun rectangle n'est null
    requires |recList| > 0 && forall r: Rectangle | r in recList :: r != null
    requires forall i | 0 <= i < |recList| :: recList[i] != null
    requires forall r: Rectangle | r in recList :: r.valid()
    requires forall i | 0 <= i < |recList| :: recList[i]!= null && 0 <= recList[i].getStartX() < recList[i].getEndX() && 0 <= recList[i].getStartY() < recList[i].getEndY()


    // modifie la couverture
    modifies this, couverture, rectangles
    ensures valid()
    {
        rectangles := recList;

        // Comme recList était valide, rectangles l'est aussi
        assert forall r: Rectangle | r in rectangles :: r.valid();
        assert forall r: Rectangle | r in rectangles :: r != null;
        assert forall i | 0 <= i < |rectangles| :: rectangles[i] != null;
        assert |rectangles| > 0;

        //initialise la taille de couverture
        setSize();

        //la liste rectangles est toujours valide
        assert |rectangles| > 0;
        assert forall i | 0 <= i < |rectangles| :: rectangles[i] != null;
        assert forall r: Rectangle | r in rectangles :: r != null;
        assert forall i | 0 <= i < |rectangles| :: rectangles[i]!= null && rectangles[i].getStartX() < couverture.Length0 && rectangles[i].getStartY() < couverture.Length1;

        var i := 0;
        var r: Rectangle;
        var tab:= rectangles;

        assert fresh(couverture);

        while(i < |rectangles|)
        invariant 0 <= i <= |rectangles| && couverture != null && forall i | 0 <= i < |rectangles| :: rectangles[i] != null
        invariant forall i | 0 <= i < |rectangles| :: rectangles[i] == tab[i];
        invariant forall i | 0 <= i < |rectangles| :: rectangles[i].getStartX() < couverture.Length0 && rectangles[i].getStartY() < couverture.Length1
        invariant forall i | 0 <= i < |rectangles| :: rectangles[i].valid()
        decreases |rectangles|-i
        modifies couverture
        {
            assert 0 <= i < |rectangles|;
            r := rectangles[i];
            assert r != null;

            if (r.getValue() == 0)
            {
                assert r.getStartX() < couverture.Length0 && r.getStartY() < couverture.Length1;
                couverture[r.getStartX(), r.getStartY()] := 0;
            }
            else
            {
                var y := r.getStartY();
                while(y < r.getEndY())
                invariant r.getStartY() <= y <= r.getEndY()
                decreases r.getEndY()-y
                modifies couverture
                {
                    var x := r.getStartX();
                    while(x < r.getEndX()-1)
                    invariant r.getStartX() <= x <= r.getEndX()
                    decreases r.getEndX()-x
                    modifies couverture
                    {
                        couverture[x+1, y] := couverture[x, y];
                        x := x + 1;
                    }
                    y := y + 1;
                }

                var x := r.getStartX();
                while(x < r.getEndX())
                invariant r.getStartX() <= x <= r.getEndX()
                decreases r.getEndX()-x
                modifies couverture
                {
                    var y := r.getStartY();
                    while(y < r.getEndY()-1)
                    invariant r.getStartX() <= x <= r.getEndX()
                    invariant r.getStartY() <= y <= r.getEndY()-1 && couverture != null
                    decreases r.getEndY()-y
                    modifies couverture
                    {
                        assert 0 <= x < couverture.Length0 && 0 <= y+1 < couverture.Length1;
                        couverture[x, y+1] := couverture[x, y];
                        y := y + 1;
                    }
                    x := x + 1;
                }
            }

            i := i + 1;
            if(i < |rectangles|){
              r := rectangles[i];
            }
        }
    }

    method setSize()

    // la list rectangle contient au moins un élément et que des rectangles non null valides
    requires |rectangles| > 0
    requires forall r: Rectangle | r in rectangles :: r != null
    requires forall r: Rectangle | r in rectangles :: r.valid()
    requires forall i | 0 <= i < |rectangles| :: rectangles[i] != null
    requires forall i | 0 <= i < |rectangles| :: rectangles[i]!= null && 0 <= rectangles[i].getStartX() < rectangles[i].getEndX() && 0 <= rectangles[i].getStartY() < rectangles[i].getEndY()


    ensures rectangles == old(rectangles)
    ensures couverture != null
    ensures fresh(couverture);
    ensures forall i | 0 <= i < |rectangles| :: rectangles[i]!= null && 0 <= rectangles[i].getStartX() < rectangles[i].getEndX() <= couverture.Length0 && 0 <= rectangles[i].getStartY() < rectangles[i].getEndY() <= couverture.Length1
    ensures valid()

    modifies this, couverture
    {
        var xMax := 1;
        var yMax := 1;
        var count := 1;
        var length := |rectangles|;
        var tab := rectangles;


        var i := 0;
        var r: Rectangle;

        while(i < length)
        invariant 0 <= i <= length && forall i | 0 <= i < |rectangles| :: rectangles[i] != null && rectangles[i] == tab[i];
        invariant forall i | 0 <= i < |rectangles| :: rectangles[i]!= null && 0 <= rectangles[i].getStartX() < rectangles[i].getEndX() && 0 <= rectangles[i].getStartY() < rectangles[i].getEndY()
        invariant xMax >= 0 && yMax >= 0;
        decreases length-i
        decreases length-xMax
        decreases length-yMax
        {
            assert 0<=i<|rectangles|;
            r := rectangles[i];
            assert r!= null;

            assert r.getEndX() > 0;
            if (r.getEndX() > xMax)
            {
                xMax := r.getEndX();
                assert xMax > 0;
            }

            assert r.getEndY() > 0;
            if (r.getEndY() > yMax)
            {
                yMax := r.getEndY();
                assert yMax > 0;
            }

            i := i + 1;
        }

        assert |rectangles| == length;
        assert xMax >= 0;
        assert yMax >= 0;

        couverture := new int[xMax, yMax];

        assert couverture != null;
        assert couverture.Length0 > 0 && couverture.Length1 > 0;

        var y := 0;
        while(y < yMax)
        invariant 0 <= y <= yMax && couverture != null && couverture.Length0 >0 && couverture.Length1 >0
        decreases yMax-y
        modifies couverture
        {
            var x := 0;
            while(x < xMax)
            invariant 0 <= x <= xMax && couverture != null && couverture.Length0 >0 && couverture.Length1 >0
            decreases xMax-x
            modifies couverture
            {
                assert x < couverture.Length0 && y < couverture.Length1;
                couverture[x, y] := count;
                assert couverture != null;
                count := count + 1;
                x := x + 1;
            }
            y := y + 1;
        }
        assert couverture != null;
        assert couverture.Length0 > 0 && couverture.Length1 > 0;
    }

    method contains(x: int, y: int) returns (b: bool)
    requires valid()
    requires 0 <= x < couverture.Length0 && 0 <= y < couverture.Length1
    ensures valid()
    {
        assert 0 <= x < couverture.Length0 && 0<= y < couverture.Length1;
        var value := find(x, y);

        if(couverture.Length0 > 1){ // correspond à couverture.length en java
            if(x == 0){
                if(couverture[x+1, y] == value){
                   return true;
                }
            }

            else if(x == couverture.Length0-1){
                if(couverture[x-1, y] == value){
                    return true;
                }
            }

            else{
                if(couverture[x-1, y] == value || couverture[x+1, y] == value)
        				{
        					 return true;
        				}
            }
        }

        if(couverture.Length1 > 1) //correspond à couverture[0].length en java
    		{
      			if(y==0)
      			{
        				if(couverture[x, y+1] == value)
        				{
        					 return true;
        				}
      			}

      			else if(y == couverture.Length1-1)
      			{
        				if(couverture[x, y-1] == value)
        				{
        					 return true;
        				}
      			}

      			else
      			{
        				if(couverture[x, y+1] == value || couverture[x, y-1] == value)
        				{
        					 return true;
        				}
      			}
    		}
    		return false;
    }

    method canMerge(r1: Rectangle, r2: Rectangle) returns (b: bool)
    requires valid()
    requires r1 != null && r2 != null
    requires r1.valid() && r2.valid()
    ensures valid()
    {
          // si c un obstacle on ne peut pas merge
          if( r1.getValue() == 0 || r2.getValue() == 0)
          {
              return false;
          }

          // teste si on peut merger horizontalment
          if((r1.getEndX() == r2.getStartX() || r1.getStartX() == r2.getEndX()) && r1.getStartY() == r2.getStartY() && r1.getEndY() == r2.getEndY())
          {
              return true;
          }

          // teste si on peut merger verticalement
          if((r1.getEndY() == r2.getStartY() || r1.getStartY() == r2.getEndY()) && r1.getStartX() == r2.getStartX() && r1.getEndX() == r2.getEndX())
          {
              return true;
          }

          return false;
    }

    function method doCanMerge(r1: Rectangle, r2: Rectangle): bool
    requires r1 != null && r2 != null
    requires r1.valid() && r2.valid()
    requires valid()
    ensures valid()
    reads this, couverture, rectangles, r1, r2
    {
        if r1.getValue() == 0 || r2.getValue() == 0 then false
        else if ((r1.getEndX() == r2.getStartX() || r1.getStartX() == r2.getEndX()) && r1.getStartY() == r2.getStartY() && r1.getEndY() == r2.getEndY())
          || ((r1.getEndY() == r2.getStartY() || r1.getStartY() == r2.getEndY()) && r1.getStartX() == r2.getStartX() && r1.getEndX() == r2.getEndX())
          then true
          else false
    }

    method merge(r1: Rectangle, r2: Rectangle) returns (r: Rectangle)
    requires valid()
    requires r1 != null && r2 != null
    requires r1.valid() && r2.valid()
    requires r1.getEndX() > r1.getStartX() >= 0 && r2.getEndX() > r2.getStartX() >= 0 && r1.getEndY() > r1.getStartY() >= 0 && r2.getEndY() > r2.getStartY() >= 0
    requires couverture.Length0 > r1.getEndX() > 0 && couverture.Length0 > r2.getEndX() > 0 && couverture.Length1 > r1.getEndY() > 0 && couverture.Length1 > r2.getEndY() > 0
    requires doCanMerge(r1, r2)

    ensures r == null || r.valid()
    ensures valid()
    modifies this, couverture
    {
        var x := r2.getStartX();
        while(x < r2.getEndX())
        invariant r2.getStartX() <= x <= r2.getEndX()
        invariant couverture != null
        invariant r1.getStartX() < couverture.Length0 && r1.getStartY() < couverture.Length1
        invariant r2.getStartX() < couverture.Length0 && r2.getStartY() < couverture.Length1
        decreases r2.getEndX()-x
        modifies couverture
        {
            var y := r2.getStartY();
            while(y < r2.getEndY())
            invariant r2.getStartY() <= y <= r2.getEndY() && couverture != null
            invariant r1.getStartX() < couverture.Length0 && r1.getStartY() < couverture.Length1
            invariant r2.getStartX() < couverture.Length0 && r2.getStartY() < couverture.Length1
            invariant x == old(x)
            decreases r2.getEndY()-y
            modifies couverture
            {
                assume 0 <= x < couverture.Length0 && 0 <= y < couverture.Length1;
                couverture[x, y] := couverture[r1.getStartX(), r1.getStartY()];
                y := y + 1;
            }
            x := x + 1;
        }

        assert couverture != null;
        assert couverture.Length0 > 0 && couverture.Length1 > 0;

        var startX := min(r1.getStartX(), r2.getStartX());
        assert startX >= 0;

        var startY := min(r1.getStartY(), r2.getStartY());
        assert startY >=0;

        var endX := max(r1.getEndX(), r2.getEndX());
        assert endX >0;

        var endY := max(r1.getEndY(), r2.getEndY());
        assert endY >0;

        var value := 1;
        assert value == 0 || value==1;

        var rectangle := new Rectangle(startX, startY, endX, endY, value);
        assert rectangle != null && rectangle.valid();

        return rectangle;
    }

    function method min(a: int, b: int): int
    {
        if a > b then b else a
    }

    function method max(a: int, b: int): int
    {
        if a > b then a else b
    }

    method improve() returns (b: bool)
    requires valid()
    requires |rectangles| > 0 ==> forall r: Rectangle | r in rectangles :: r != null
    requires forall i | 0 <= i < |rectangles| :: rectangles[i] != null
    requires forall r: Rectangle | r in rectangles :: r.valid()
    requires forall r: Rectangle | r in rectangles :: (couverture.Length0 > r.getEndX() > r.getStartX() >= 0 && couverture.Length1 > r.getEndY() > r.getStartY() >= 0)
    ensures valid()
    ensures b == false || b == true
    modifies this, couverture
    {
        var index1 := 0;
        var index2 := 0;

        var i := 0;
        while(i < |rectangles|)
        invariant 0<=i<=|rectangles|
        invariant couverture !=null && couverture.Length0 > 0 && couverture.Length1 > 0
        decreases |rectangles|-i
        {
            var j := i + 1;
            while(j < |rectangles|)
            invariant i+1<=j<=|rectangles|
            decreases |rectangles|-j
            {
                assert i < |rectangles| && j < |rectangles|;

                var r1: Rectangle := rectangles[i];
                var r2: Rectangle := rectangles[j];

                assert r1 != null && r2 != null;
                assert r1.valid() && r2.valid();
                assert 0 <= r1.getStartX() < r1.getEndX() < couverture.Length0 && 0 <= r1.getStartY() < r1.getEndY() < couverture.Length1;
                assert 0 <= r2.getStartX() < r2.getEndX() < couverture.Length0 && 0 <= r2.getStartY() < r2.getEndY() < couverture.Length1;
                if(|rectangles| > 1 && doCanMerge(rectangles[i], rectangles[j])){

                    //take the first i elements and drop the first i+1 elements
                    //then concatenate them to obtain a list without the i th value?
                    rectangles := rectangles[..i] + rectangles[i+1..];
                    //same process
                    if(i < j) { j := j - 1;}
                    rectangles := rectangles[..j] + rectangles[j+1..];
                    var newR: Rectangle := merge(r1, r2);
                    rectangles := rectangles + [newR];

                    return true;
                }
                j := j + 1;
            }
            i := i + 1;
        }
        return false;
    }

    method optimize()
    requires valid()
    requires forall i | 0 <= i < |rectangles| :: rectangles[i] != null
    requires forall r: Rectangle | r in rectangles :: r.valid()
    requires forall r: Rectangle | r in rectangles :: (couverture.Length0 > r.getEndX() > r.getStartX() >= 0 && couverture.Length1 > r.getEndY() > r.getStartY() >= 0)
    modifies this, couverture, rectangles
    {
        var b: bool := improve();

        while(b)
        //invariant forall i | 0 <= i < |rectangles| :: rectangles[i] != null && rectangles[i].valid()
        //invariant couverture != null && couverture.Length0 > 0 && couverture.Length1 > 0
        invariant b <==> (false || true)
        modifies this, couverture, rectangles
        {
           b := improve();
        }
        return;
    }

    //*************************************************************************
    //Union-Find Methods
    //*************************************************************************

    function method find(a: int, b: int): int
    requires valid() && 0 <= a < couverture.Length0 && 0 <= b < couverture.Length1
    ensures valid()
    ensures couverture != null
    reads this, couverture, rectangles
    {
        couverture[a, b]
    }

    method union(a: int, b: int, c: int, d: int)
    requires valid()
    requires 0 <= a < couverture.Length0 && 0 <= b < couverture.Length1 && 0 <= c < couverture.Length0 && 0 <= d < couverture.Length1
    modifies couverture
    {
        if( connected(a,  b,  c,  d)){
            return;
        }

        var qId := find(a, b);
        var pId := find(c, d);

        if(pId == qId) { return; }
        var x := 0;
        while(x < couverture.Length0)
        invariant couverture!=null
        invariant 0 <= x <= couverture.Length0
        decreases couverture.Length0-x
        modifies couverture
        {
            assert x < couverture.Length0;
            var y := 0;

            while(y < couverture.Length1)
            invariant couverture != null
            invariant 0 <= y <= couverture.Length1
            invariant 0 <= x <= couverture.Length0
            decreases couverture.Length1-y
            modifies couverture
            {
                assert x < couverture.Length0;
                assert y < couverture.Length1;
                if(couverture[x, y] == pId)
                {
                    couverture[x, y] := qId;
                }
                y := y + 1;
            }
            x := x + 1;
        }
    }

    function method connected(a: int, b: int, c: int, d: int): bool
    requires valid()
    requires 0 <= a < couverture.Length0 && 0 <= b < couverture.Length1 && 0 <= c < couverture.Length0 && 0 <= d < couverture.Length1
    ensures valid()
    reads this, couverture, rectangles
    {
        find(a, b) == find(c, d)
    }
}