// A nice idiomatic imperative implementation of reachability checking.

// Given that CanReach discovers the sort of paths that satisfy ReachableNoDupWithout,
// complete the loop invariant such that:
//  - Dafny agrees that the `return false` satisfies the postcondition
//  - by invoking a lemma before the loop, Dafny agrees your invariant is *established*
//  - by providing a witness in the `next == dst` block, Dafny agrees that the
//    `return true` satisfies the postcondition
//  - ... and if you have all of those pieces, you can get started on the proof that
//    your invariant is *maintained* by the loop!

method CanReach(g: Graph, src: Node, dst: Node) returns (b: bool)
  requires src in Nodes(g)
  ensures b == Reachable(g, src, dst)
{
  var frontier := {src};
  var visited := {};
  while |frontier| > 0
    invariant frontier + visited <= Nodes(g)
    invariant frontier !! visited
    invariant Reachable(g, src, dst) <==> ???
    decreases Nodes(g) - visited
  {
    var next :| next in frontier;
    if next == dst {
      return true;
    }
    frontier := frontier - {next};
    visited := visited + {next};
    frontier := frontier + (set e | e in g && e.0 == next && e.1 !in visited :: e.1);
  }
  return false;
}

// === Graph definitions ===

type Node = int
type Edge = (Node, Node)
type Graph = set<Edge>

function Nodes(graph: Graph): set<Node> {
  (set edge | edge in graph :: edge.0) + (set edge | edge in graph :: edge.1)
}

// === Reachability ===

ghost predicate Reachable(graph: Graph, src: Node, dst: Node) {
  exists path: seq<Node> ::
    && |path| >= 1
    && path[0] == src
    && path[|path|-1] == dst
    && (forall i :: 0 <= i < |path|-1 ==> (path[i], path[i+1]) in graph)
}

ghost predicate ReachableNoDup(g: Graph, src: Node, dst: Node) {
  exists path: seq<Node> ::
    && |path| >= 1 && path[0] == src && path[|path|-1] == dst
    && (forall i :: 0 <= i < |path|-1 ==> (path[i], path[i+1]) in g)
    && (forall i, j :: 0 <= i < j < |path| ==> path[i] != path[j])
}

lemma ReachableNoDupEquiv(g: Graph, src: Node, dst: Node)
  ensures ReachableNoDup(g, src, dst) == Reachable(g, src, dst)

ghost predicate ReachableNoDupWithout(g: Graph, src: Node, dst: Node, visited: set<Node>) {
  exists path: seq<Node> ::
    && |path| >= 1 && path[0] == src && path[|path|-1] == dst
    && (forall i :: 0 <= i < |path|-1 ==> (path[i], path[i+1]) in g)
    && (forall i, j :: 0 <= i < j < |path| ==> path[i] != path[j])
    && (forall n :: n in path ==> n !in visited)
}