sig City {roads: set City} run {} for exactly 6 City fact roadsGoSomewhere { no iden & roads } pred isCycle[cities: set City] { -- not this: -- cities in cities.^roads let localRoads = roads & cities->cities | all c: cities | all c2: cities-c | c2 in c.^localRoads } pred testCounterexample { some disj a, b, c, d: City | { roads = a->b + b->a + c->d + d->c isCycle[a+b+c+d] } } run testCounterexample for exactly 4 City -------------------------------------- fun neighborsOfSet[cities: set City]: set City { cities.roads } fun evenHops[cities: set City]: set City->City { --let localRoads = (cities <: roads) & (roads :> cities) | let localRoads = roads & cities->cities | ^(localRoads.localRoads) } run {} for exactly 4 City fun pathsAbove1A[cities: set City]: City->City { // ^r = r + r.r + r.r.r + ... let localRoads = roads & cities->cities | ^localRoads - localRoads } fun pathsAbove1B[cities: set City]: City->City { let localRoads = roads & cities->cities | evenHops[cities].localRoads + evenHops[cities] } fun pathsAbove1C[cities: set City]: City->City { let localRoads = roads & cities->cities | localRoads.^localRoads } pred compareAB { some cities: set City | not (pathsAbove1A[cities] = pathsAbove1B[cities]) } run compareAB for exactly 4 City pred compareBC { some cities: set City | not (pathsAbove1B[cities] = pathsAbove1C[cities]) } run compareBC for 5 City