#lang forge
/**
A Mesh represents a finite element mesh which is
composed of a collection of contiguous, non-overlapping
triangles. The triangles field associates a set of
Triangles with a mesh, and the adj field defines how
triangles are arranged by describing their adjacency.
*/
sig Mesh {
triangles: set Triangle,
adj: set Triangle -> Triangle
}
/**
A Triangle represents a single triangle in a Mesh, and
the edges field defines the three directed edges that
comprise a single Triangle.
*/
sig Triangle {
edges: set Vertex -> Vertex
}
/**
A Vertex represents a single discrete point
*/
sig Vertex {}
-------------------------------------------------------------------------------------
-- return the domain of a binary relation
fun dom [r: univ->univ] : set (r.univ) { r.univ }
-- return the domain of a ternary relation
fun dom3 [r: univ->univ->univ] : set((r.univ).univ) { (r.univ).univ }
-- return the range of a binary relation
fun ran [r: univ->univ] : set (univ.r) { univ.r }
-- the number of "undirected" edges (considering interior ones as half edges)
fun undirectedEdges [m: Mesh]: Int { subtract[#m.triangles.edges, divide[#m.adj, 2]] }
-- the edge set e forms a ring
pred ring [e: Vertex->Vertex] { all v: dom[e] | one v.e and dom[e] in v.^e }
-- r is symmetric
pred symmetric [r: univ -> univ] { ~r in r }
-- r is irreflexive
pred irreflexive [r: univ -> univ] { no iden & r }
-- a strongly connected digraph is a directed graph in which it is possible
-- to reach any node starting from any other node by traversing edges in
-- the direction(s) in which they point
pred stronglyConnected [r: univ -> univ, s: set univ] {
all x, y: s | x in y.*r
}
pred meshInvariants {
all m: Mesh | some m.triangles -- meshes have at least one triangle
all t: Triangle | t in Mesh.triangles -- every triangle appears in a mesh
all v: Vertex | v in dom[Mesh.triangles.edges] -- every vertex appears in a triangle
all t: Triangle | #t.edges = 3 -- every triangle has 3 edges
all t: Triangle | ring[t.edges] -- the edge set of each triangle forms a ring
all m: Mesh | all a, b: m.triangles | not a = b => no a.edges & b.edges -- no two triangles in the same mesh can share the same edge
all m: Mesh | dom[m.adj] + ran[m.adj] in m.triangles -- triangles in the m.adj relation must be in the set m.triangles
all m: Mesh | let r = m.adj, s = m.triangles | symmetric[r] and irreflexive[r] and stronglyConnected[r, s] -- properties of the dual of a mesh, viewing triangles as dual nodes
all m: Mesh, a, b: m.triangles | a in m.adj[b] iff one ~(a.edges) & b.edges -- triangles that share a pair of incident vertices define the adj relation
all m: Mesh | let T = #m.triangles, E = undirectedEdges[m], V = #dom[m.triangles.edges] | -- Euler's formula: T - 1 = E - V
subtract[T, 1] = subtract[E, V]
}
-------------------------------------------------------------------------------------
-- The set of all nodes in a mesh
fun nodes [m: one Mesh]: set Node { dom[m.triangles.edges] }
-- The set of all elements in a mesh
fun elements [m: one Mesh]: set Element { m.triangles }
/**
A number of properties we will be modeling
are simple boolean states. For example, a node
can be either wet (true) or dry (not wet, false).
*/
abstract sig Bool {}
one sig True extends Bool {}
one sig False extends Bool {}
/**
Next, we need to be able to represent water levels at each node.
We're not actually concerned with the numerical value, however,
just its relation to the value of Hmin. Inspecting the algorithm,
we see that in part 1 we check if a node's water level is less than Hmin,
and in part 3 we check if a node's water level is less than 1.2 * Hmin.
Therefore we need to represent three possible water levels:
* H < Hmin
* Hmin < H < 1.2Hmin
* 1.2Hmin < H
Create an abstract signature, Height, and extend it to create signatures
that represent these water levels, let's call them Low, Med, and High.
*/
abstract sig Height {}
one sig Low extends Height {}
one sig Med extends Height {}
one sig High extends Height {}
/**
The nodes of our mesh have three properties that are used in the wet/dry algorithm:
* W: the wet/dry status of the node
* Wt: the temporary wet/dry status of the node
* H: the water level of the node
During a single execution of the wet/dry algorithm, H is constant
while W and Wt may change, so we only add H to our Node signature.
*/
sig Node extends Vertex {
H: one Height
}
/**
The elements of our mesh also have three properties that are used in the wet/dry algorithm:
* wet: the wet/dry status of the element
* slowFlow: a boolean indicating if flow across element is slow
* lowNode: the element's node with the lowest water surface elevation
During a single execution of the wet/dry algorithm, slowFlow and lowNode are unchanged,
so we add them to our Element declaration.
*/
sig Element extends Triangle {
slowFlow: one Bool,
lowNode: one Node
}
/**
Our state signature include the "dynamic" properties of nodes and element --- those
that are changed at some point during the execution of the wet/dry algorithm.
Additionally, we include a step field (indicating the current step of the algorithm)
and an m field (indicating the relevant mesh).
*/
sig State {
step: one Int,
m: one Mesh,
W: set Node -> Bool,
Wt: set Node -> Bool,
wet: set Element -> Bool
}
pred wetdryInvariants {
Bool = True + False -- booleans can be true or false
Height = Low + Med + High -- water levels can be low, medium, or height
all v: Vertex | v in Node -- all vertices are nodes
all t: Triangle | t in Element -- all triangles are elements
all e: Element | e.lowNode in dom[e.edges] -- each element, the low node is incident
-- all three of our boolean properties must be exactly true or false
all s: State {
let mesh = s.m {
all n: nodes[mesh] | one s.W[n] and one s.Wt[n]
all e: elements[mesh] | one s.wet[e]
}
}
}
------------------- Helper predicates -----------------------
-- the number of wet nodes in an element
fun wetNodes [e: Element, s: State]: Int {
let n = dom[e.edges], w = s.W.True | #(n & w)
}
-- an element has exactly one dry node
pred loneDryNode [n: Node, e: Element, s: State] {
n in dom[e.edges] and n.W[s] = False and wetNodes[e, s] = 2
}
/**
* Define the conditions that cause a node to become wet. For a
* node to become wet, it must be part of an element with sufficient
* water velocity and that has a single dry node.
*/
pred make_wet [m: Mesh, n: Node, s: State] {
some e: elements[m] |
e.slowFlow = False and loneDryNode[n, e, s]
}
-- an element is active
pred active [e: Element, s: State] {
e.wet[s] = True
all n: dom[e.edges] | n.Wt[s] = True
}
-- a node is landlocked
pred landlocked [m: Mesh, n: Node, s: State] {
no { e: elements[m] | n in dom[e.edges] and active[e, s] }
}
/**
* Define the conditions that cause a node to become dry.
*/
pred make_dry [m: Mesh, n: Node, s: State] {
n.Wt[s] = True and landlocked[m, n, s]
}
/**
A predicate that we can use to define a total ordering of States
using integer indexing. The integer i specifies the index of the post-state
*/
pred ordering [pre: State, post: State, i: Int] {
pre.m = post.m
pre.step = post.step.~succ
post.step = sing[i]
}
---------------- The steps of the wet/dry algorithm -----------------
state[State] part0 {
step = sing[0]
nodes[m].W = nodes[m].Wt
}
transition[State] part1 {
ordering[this, this', 1]
elements[m].wet = elements[m].wet'
/**
* Fill in part 1
*/
}
transition[State] part2 {
ordering[this, this', 2]
elements[m].wet = elements[m].wet'
/**
* Fill in part 2
* Note: the make_wet predicate defines the conditions that
* cause a node to become (temporarily) wet.
*/
}
transition[State] part3 {
ordering[this, this', 3]
all n: nodes[m] | n.W' = n.W and n.Wt' = n.Wt
/**
* Fill in part 3
*/
}
transition[State] part4 {
ordering[this, this', 4]
elements[m].wet' = elements[m].wet
/**
* Fill in part 4
* Note: the make_dry predicate defines the conditions that
* cause a node to become (temporarily) dry.
*/
}
transition[State] part5 {
ordering[this, this', 5]
elements[m].wet' = elements[m].wet
/**
* Fill in part 5
*/
}
----------- Build some traces and answer some questions --------------
-- Define an initial state in which all nodes are dry
state[State] initAllDry {
part0[this]
all n: nodes[m] | n.W = False
}
-- Define an initial state in which all nodes are wet
state[State] initAllWet {
part0[this]
all n: nodes[m] | n.W = True
}
-- Define a final state in which all nodes are dry
state[State] endAllDry {
all n: nodes[m] | n.W = False
}
-- Define a final state in which all nodes are wet
state[State] endAllWet {
all n: nodes[m] | n.W = True
}
-- Define a transition predicate that allows one of our algorithm steps to be used.
-- Because we have defined a total ordering of states using integer indexing, a
-- scope of exactly 6 State will give us a trace in which each step of the algorithm
-- is "executed" in the proper order, beginning with the initial state.
transition[State] advance {
part1[this, this'] or
part2[this, this'] or
part3[this, this'] or
part4[this, this'] or
part5[this, this']
}
-- Can a mesh start out with all dry nodes and have them all become wet?
trace<|State, initAllDry, advance, endAllWet|> allDryToWet {}
run<|allDryToWet|> {
meshInvariants
wetdryInvariants
} for exactly 1 Mesh, exactly 6 State
-- Can a mesh start out with all wet nodes and have them all become dry?
--trace<|State, initAllWet, advance, endAllDry|> allWetToDry {}
--run<|allWetToDry|> {
-- meshInvariants
-- wetdryInvariants
--} for exactly 1 Mesh, exactly 6 State, 1 Triangle
-- Generate a valid trace
--trace<|State, part0, advance, _|> wetdry {}
--run<|wetdry|> {
-- meshInvariants
-- wetdryInvariants
--} for exactly 1 Mesh, exactly 6 State
----------------------------------------------------------------------------
state[State] initAnswerQuestion {
part0[this]
all n: nodes[m] | n.W = True
all e: elements[m] | e.slowFlow = True and e.wet = True
some n: Node | one e: elements[m] | e.lowNode != n
}
transition[State] advanceAnswerQuestion {
nodes[m].W' = nodes[m].W
nodes[m].Wt' = nodes[m].Wt
part1[this, this'] or
part2[this, this'] or
part3[this, this'] or
part4[this, this'] or
part5[this, this']
}
state[State] dryElementWetNodes {
one e: elements[m] | e.wet = False and wetNodes[e, this] = 3
}
-- Is it possible for an element with three wet nodes to become dry?
-- Which step of the algorithm causes an element with three temporarily wet nodes to become dry?
trace<|State, initAnswerQuestion, advanceAnswerQuestion, dryElementWetNodes|> answer {}
run<|answer|> {
meshInvariants
wetdryInvariants
} for exactly 1 Mesh, exactly 6 State, exactly 3 Element, exactly 4 Node