?prevdifflink? - Blame
values
max: nat = 10
types
N = nat
inv n == n < max;
NPoint ::
x : N
y : N;
NSeg ::
pts: set of NPoint
inv mk_NSeg(ps) == card ps = 2
functions
SelPoints: NSeg -t> NPoint * NPoint
SelPoints(mk_NSeg(pts)) ==
let p in set pts
in
let q in set pts \ {p}
in
mk_(p,q)
functions
Points: NSeg -t> set of NPoint
Points(s) ==
let mk_(p1,p2) = SelPoints(s)
in
{mk_NPoint(x,y)| x in set DiffX(p1,p2), y in set DiffY(p1,p2) &
let p = mk_NPoint(x,y) in
RatEq(Slope(p,p1),Slope(p2,p)) or p = p1 or p = p2}
types
Rat = int * int
functions
Slope: NPoint * NPoint -t> Rat
Slope(mk_NPoint(x1,y1),mk_NPoint(x2,y2)) ==
mk_((y2-y1),(x2-x1));
RatEq: Rat * Rat -t> bool
RatEq(mk_(x1,y1),mk_(x2,y2)) ==
x1 * y2 = x2 * y1;
DiffX: NPoint * NPoint -t> set of N
DiffX(mk_NPoint(x1,-),mk_NPoint(x2,-)) ==
if x1 < x2
then {x1,...,x2}
else {x2,...,x1};
DiffY: NPoint * NPoint -t> set of N
DiffY(mk_NPoint(-,y1),mk_NPoint(-,y2)) ==
if y1 < y2
then {y1,...,y2}
else {y2,...,y1};
On: NPoint * NSeg -t> bool
On(p,s) ==
p in set Points(s);
In: NPoint * NSeg -t> bool
In(p,s) ==
On(p,s) and p not in set s.pts;
Meet: NSeg * NSeg -t> bool
Meet(mk_NSeg(pts1),mk_NSeg(pts2)) ==
card (pts1 inter pts2) = 1;
Parallel: NSeg * NSeg -t> bool
Parallel(s,t) ==
let mk_(p1,p2) = SelPoints(s),
mk_(p3,p4) = SelPoints(t)
in
Slope(p1,p2) = Slope(p3,p4);
Overlap: NSeg * NSeg -t> bool
Overlap(s1,s2) ==
card (Points(s1) inter Points(s2)) > 1;
Aligned: NSeg * NSeg -t> bool
Aligned(s1,s2) ==
Coliner(s1,s2) and (not Overlap(s1,s2));
Intersect: NSeg * NSeg -t> bool
Intersect(s,t) ==
let mk_(mk_NPoint(x11,y11),mk_NPoint(x12,y12)) = SelPoints(s),
mk_(mk_NPoint(x21,y21),mk_NPoint(x22,y22)) = SelPoints(t)
in
let a11 = x11 - x12,
a12 = x22 - x21,
a21 = y11 - y12,
a22 = y22 - y21,
b1 = x11 - x21,
b2 = y11 - y21
in
let d1 = b1 * a22 - b2 * a12,
d2 = b2 * a11 - b1 * a21,
d = a11 * a22 - a12 * a21
in
d <> 0 and
(let l = d1 / d,
m = d2 / d
in
0 < l and l < 1 and
0 < m and m < 1);
Coliner: NSeg * NSeg -t> bool
Coliner(s,t) ==
let mk_(p1,p2) = SelPoints(s),
mk_(p3,p4) = SelPoints(t)
in
RatEq(Slope(p1,p2),Slope(p3,p4)) and
(RatEq(Slope(p1,p3),Slope(p1,p4)) or
RatEq(Slope(p3,p1),Slope(p1,p4)));
Disjoint: NSeg * NSeg -t> bool
Disjoint(s1,s2) ==
s1 <> s2 and (not Meet(s1,s2)) and (not Intersect(s1,s2));
Intersection: NSeg * NSeg -> NPoint
Intersection(s,t) ==
let mk_(mk_NPoint(x11,y11),mk_NPoint(x12,y12)) = SelPoints(s),
mk_(mk_NPoint(x21,y21),mk_NPoint(x22,y22)) = SelPoints(t)
in
let a11 = x11 - x12,
a12 = x22 - x21,
a21 = y11 - y12,
a22 = y22 - y21,
b1 = x11 - x21,
b2 = y11 - y21
in
let d1 = b1 * a22 - b2 * a12,
d = a11 * a22 - a12 * a21
in
if d <> 0
then let x0 = x11 * d + d1 * (x12 - x11),
y0 = y11 * d + d1 * (y12 - y11)
in
mk_NPoint(RoundToN(abs x0,abs d),RoundToN(abs y0,abs d))
else undefined
pre Intersect(s,t);
RoundToN: nat * nat -t> nat
RoundToN(a,b) ==
let mk_(z,aa) = if a >= b
then mk_(a div b, a mod b)
else mk_(0,a)
in
if aa = 0 or 2 * aa <= b
then z
else z + 1
types
Realm ::
points: set of NPoint
segs : set of NSeg
inv mk_Realm(ps,ss) ==
(forall mk_NSeg(pts) in set ss & pts subset ps) and
(forall s in set ss, p in set ps & not In(p,s)) and
(forall s1,s2 in set ss & s1 <> s2 => (not Intersect(s1,s2) and (not Overlap(s1,s2))))
functions
InsertNPoint: Realm * NPoint -t> Realm
InsertNPoint(mk_Realm(ps,ss),p) ==
if p in set ps
then mk_Realm(ps,ss)
elseif forall s in set ss & p not in set E(s)
then mk_Realm(ps union {p},ss)
else let s_env = {s|s in set ss & p in set E(s)}
in
let ss1 = dunion{{mk_NSeg({p1,p}),mk_NSeg({p,p2})}
|mk_NSeg({p1,p2}) in set s_env
& p not in set {p1,p2}}
in
mk_Realm(ps union {p},(ss union ss1)\s_env)
pre not (exists s in set ss & In(p,s));
InsertNSegment: Realm * NSeg -t> Realm
InsertNSegment(mk_Realm(ps,ss),s) ==
if s in set ss
then mk_Realm(ps,ss)
elseif (forall p in set ps & p not in set E(s)\EndPoints(ss)) and
(forall t in set ss & (not Intersect(s,t)) and (not Overlap(s,t)))
then mk_Realm(ps,ss union {s})
else let p_env = {p | p in set ps inter E(s)}\EndPoints(ss),
s_inter = {t|t in set ss & Intersect(s,t)}
in
let ss1 = ChopNPoints(p_env,{s})
in
let mk_(new_ps, new_ss) = ChopNSegs(ss, s_inter,ss1,{})
in
mk_Realm(ps union new_ps,new_ss)
pre s.pts subset ps;
ChopNPoints: set of NPoint * set of NSeg -t> set of NSeg
ChopNPoints(ps,ss) ==
if ps = {}
then ss
else let p in set ps
in
let s_env = {s | s in set ss & p in set E(s) and
p not in set s.pts}
in
let s in set s_env
in
let mk_(p1,p2) = SelPoints(s)
in
ChopNPoints(ps\{p},(ss \{s}) union {mk_NSeg({p1,p}),mk_NSeg({p2,p})})
pre forall p in set ps & exists s in set ss & p in set E(s) and p not in set s.pts;
ChopNSegs: set of NSeg * set of NSeg * set of NSeg * set of NPoint -t>
set of NPoint * set of NSeg
ChopNSegs(ss,s_inter,newss,ps) ==
if s_inter = {}
then mk_(ps,ss union newss)
else let t in set s_inter
in
let {s} = {s |s in set newss & Intersect(s,t)}
in
let p = Intersection(t,s)
in
let chop_s = {mk_NSeg({p,sp})|sp in set s.pts & p <> sp},
chop_t = {mk_NSeg({p,tp})|tp in set t.pts & p <> tp}
in
ChopNSegs((ss \ {t}) union chop_t,
s_inter\{t}, (newss \ {s}) union chop_s, ps union{p});
E: NSeg -t> set of NPoint
E(s) ==
let mk_(p1,p2) = SelPoints(s)
in
{mk_NPoint(x,y) | x in set DiffX(p1,p2), y in set DiffY(p1,p2) &
(0 < y and y < max - 1 and
Intersect(mk_NSeg({mk_NPoint(x,y-1),mk_NPoint(x,y+1)}),s)) or
(0 < x and x < max - 1 and
Intersect(mk_NSeg({mk_NPoint(x-1,y),mk_NPoint(x+1,y)}),s))};
EndPoints: set of NSeg -> set of NPoint
EndPoints(ss) ==
dunion{pts|mk_NSeg(pts) in set ss};
CycleCheck: set of NSeg -t> bool
CycleCheck(ss) ==
exists sl in set AllLists(ss) &
forall i in set inds sl &
Meet(sl(i),sl(if i = len sl then 1 else i+1)) and
(forall j in set inds sl \ {if i = 1 then len sl else i-1,
i,
if i = len sl then 1 else i+1} &
not Meet(sl(i),sl(j)));
AllLists: set of NSeg -t> set of seq of NSeg
AllLists(ss) ==
cases ss:
{i} -> {[]},
{s} -> {[s]},
others -> dunion {{[s]^l |
l in set AllLists(ss \{s})} |
s in set ss}
end
types
Cycle = set of NSeg
inv ss == CycleCheck(ss)
functions
OnCycle: NPoint * Cycle -t> bool
OnCycle(p,c) ==
exists s in set c & On(p,s);
InsideCycle: NPoint * Cycle -t> bool
InsideCycle(p,c) ==
not OnCycle(p,c) and IsOdd(card SR(p,c) + card SI(p,c)) ;
OutsideCycle: NPoint * Cycle -t> bool
OutsideCycle(p,c) ==
not (OnCycle(p,c) or InsideCycle(p,c));
SR: NPoint * Cycle -t> set of NSeg
SR(p,ss) ==
{s | s in set ss & let mk_(p1,p2) = SelPoints(s)
in
(p.y < max - 1 and (not On(p1,SP(p))) and On(p2,SP(p))) or
(p.y < max - 1 and (not On(p2,SP(p))) and On(p1,SP(p)))}
pre CycleCheck(ss);
SI: NPoint * Cycle -t> set of NSeg
SI(p,ss) ==
{s | s in set ss & p.y < max - 1 and Intersect(s,SP(p))};
SP: NPoint -t> NSeg
SP(mk_NPoint(x,y)) ==
mk_NSeg({mk_NPoint(x,y),mk_NPoint(x,max - 1)})
pre y < max - 1;
IsOdd: nat -t> bool
IsOdd(n) ==
n mod 2 <> 0;
Partition: (NPoint * set of NSeg -> bool) * Cycle -t> set of NPoint
Partition(pred,ss) ==
{mk_NPoint(x,y) | x in set {0,...,max-1}, y in set {0,...,max-1} &
pred(mk_NPoint(x,y),ss)};
P: Cycle -t> set of NPoint
P(ss) ==
Partition(OnCycle,ss) union Partition(InsideCycle,ss);
AreaInside: Cycle * Cycle -t> bool
AreaInside(c1,c2) ==
P(c1) subset P(c2);
EdgeInside: Cycle * Cycle -t> bool
EdgeInside(c1,c2) ==
AreaInside(c1,c2) and c1 inter c2 = {};
VertexInside: Cycle * Cycle -t> bool
VertexInside(c1,c2) ==
EdgeInside(c1,c2) and
Partition(OnCycle,c1) inter Partition(OnCycle,c2) = {};
AreaDisjoint: Cycle * Cycle -t> bool
AreaDisjoint(c1,c2) ==
Partition(InsideCycle,c1) inter P(c2) = {} and
Partition(InsideCycle,c2) inter P(c1) = {};
EdgeDisjoint: Cycle * Cycle -t> bool
EdgeDisjoint(c1,c2) ==
AreaDisjoint(c1,c2) and c1 inter c2 = {};
VertexDisjoint: Cycle * Cycle -t> bool
VertexDisjoint(c1,c2) ==
P(c1) inter P(c2) = {};
AdjacentCycles: Cycle * Cycle -t> bool
AdjacentCycles(c1,c2) ==
AreaDisjoint(c1,c2) and c1 inter c2 <> {};
MeetCycles: Cycle * Cycle -t> bool
MeetCycles(c1,c2) ==
EdgeDisjoint(c1,c2) and
Partition(OnCycle,c1) inter Partition(OnCycle,c2) <> {};
SAreaInside: NSeg * Cycle -t> bool
SAreaInside(s,c) ==
let mk_(p1,p2) = SelPoints(s)
in
PAreaInside(p1,c) and PAreaInside(p2,c);
SEdgeInside: NSeg * Cycle -t> bool
SEdgeInside(s,c) ==
let mk_(p1,p2) = SelPoints(s)
in
(PAreaInside(p1,c) and PVertexInside(p2,c)) or
(PAreaInside(p2,c) and PVertexInside(p1,c));
SVertexInside: NSeg * Cycle -t> bool
SVertexInside(s,c) ==
let mk_(p1,p2) = SelPoints(s)
in
PVertexInside(p1,c) and PVertexInside(p2,c);
PAreaInside: NPoint * Cycle -t> bool
PAreaInside(p,c) ==
p in set P(c);
PVertexInside: NPoint * Cycle -t> bool
PVertexInside(p,c) ==
p in set Partition(InsideCycle,c)
types
Face :: c : Cycle
hs : set of Cycle
inv mk_Face(c,hs) ==
(forall h in set hs & EdgeInside(h,c)) and
(forall h1,h2 in set hs & h1 <> h2 => EdgeDisjoint(h1,h2)) and
(forall ss in set power (c union dunion hs) &
CycleCheck(ss) => ss in set hs union {c})
functions
PAreaInsideF: NPoint * Face -t> bool
PAreaInsideF(p,mk_Face(c,hs)) ==
PAreaInside(p,c) and (forall h in set hs & not PVertexInside(p,h));
SAreaInsideF: NSeg * Face -t> bool
SAreaInsideF(s,mk_Face(c,hs)) ==
SAreaInside(s,c) and (forall h in set hs & not SEdgeInside(s,h));
FAreaInside: Face * Face -t> bool
FAreaInside(mk_Face(c1,hs1),mk_Face(c2,hs2)) ==
AreaInside(c1,c2) and
(forall h2 in set hs2 & AreaDisjoint(h2,c1) or
(exists h1 in set hs1 & AreaInside(h2,h1)));
FAreaDisjoint: Face * Face -t> bool
FAreaDisjoint(mk_Face(c1,hs1),mk_Face(c2,hs2)) ==
AreaDisjoint(c1,c2) or
(exists h2 in set hs2 & AreaInside(c1,h2)) or
(exists h1 in set hs1 & AreaInside(c2,h1));
FEdgeDisjoint: Face * Face -t> bool
FEdgeDisjoint(mk_Face(c1,hs1),mk_Face(c2,hs2)) ==
EdgeDisjoint(c1,c2) or
(exists h2 in set hs2 & EdgeInside(c1,h2)) or
(exists h1 in set hs1 & EdgeInside(c2,h1))
values
p1: NPoint = mk_NPoint(1,1);
p2: NPoint = mk_NPoint(5,3);
p3: NPoint = mk_NPoint(1,9);
p4: NPoint = mk_NPoint(2,3);
p5: NPoint = mk_NPoint(9,5);
p6: NPoint = mk_NPoint(6,9);
p7: NPoint = mk_NPoint(4,5);
p8: NPoint = mk_NPoint(4,6);
p9: NPoint = mk_NPoint(1,6);
p10:NPoint = mk_NPoint(5,0);
p11:NPoint = mk_NPoint(5,1);
p12:NPoint = mk_NPoint(6,0);
p13:NPoint = mk_NPoint(6,1);
s1: NSeg = mk_NSeg({p1,p2});
s2: NSeg = mk_NSeg({p1,p3});
s3: NSeg = mk_NSeg({p2,p4});
s4: NSeg = mk_NSeg({p4,p3});
s5: NSeg = mk_NSeg({p3,p2});
s6: NSeg = mk_NSeg({p5,p4});
s7: NSeg = mk_NSeg({p6,p1});
s8: NSeg = mk_NSeg({p5,p3});
s9: NSeg = mk_NSeg({p5,p7});
s10:NSeg = mk_NSeg({p9,p3});
s11:NSeg = mk_NSeg({p10,p8});
s12:NSeg = mk_NSeg({p1,p5});
s13:NSeg = mk_NSeg({p10,p13});
s14:NSeg = mk_NSeg({p11,p12});
r1: Realm = mk_Realm({p1,p2},{s1});
r2: Realm = mk_Realm({p5,p4},{s6});
r3: Realm = mk_Realm({p5,p4,p3},{s6,s8});
r4: Realm = mk_Realm({p1,p3,p4,p5,p6,p7,p8},{s6,s8});
r5: Realm = mk_Realm({p10,p13},{s13})
|