You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 
 
 
 
 

38 lines
719 B

vocabulary V {
type Node
Edge(Node, Node)
EdgeOnPath(Node, Node)
Start:Node
End:Node
// Extra symbols if needed
}
theory PathTheory : V {
// Theory expressing that EdgeOnPath is a path:
// EdgeOnPath consists of a subset of the edges that together form a loopfree path from Start to End,
// i.e., no loops, no splittings or edges coming together (each node on the path has at most one incoming and outgoing edge)
// and it starts in Start and ends in End
}
term Length : V {
// fill in
}
structure S : V {
Node = {1..7}
Edge = {1,2;2,3;3,4;4,5;5,2;5,1;4,2;2,5;6,7}
Start = 1
End = 5
}
include <mx>
procedure main() {
stdoptions.nbmodels = 0
printmodels(minimize(PathTheory, S, Length))
}