RiSE4fun samples for FormulaList of built-in samples for the Formula in RiSE4funen-USrise4fun &copy; 2017 Microsoft Corporationhttp://rise4fun.com//Images/Rise.gifRiSE4fun samples for Formulahttp://rise4fun.com/Formula/MapColoringMapColoringdomain MapColoring { Color ::= { red, green, blue, gray }. primitive AT ::= (Color). primitive BE ::= (Color). primitive CH ::= (Color). primitive DE ::= (Color). primitive DK ::= (Color). primitive FR ::= (Color). primitive LU ::= (Color). primitive NL ::= (Color). conforms := AT(at_), BE(be), CH(ch), DE(de), DK(dk), FR(fr), LU(lu), NL(nl), at_ != ch, at_ != de, be != de, be != fr, be != lu, be != nl, ch != de, ch != fr, de != dk, de != fr, de != lu, de != nl, fr != lu. } partial model Map of MapColoring { AT(_) BE(_) CH(_) DE(_) DK(_) FR(_) LU(_) NL(_) } http://rise4fun.com/Formula/MoreMoneyMoreMoneydomain MoreMoney { Digits ::= { 0, 1, 2, 3, 4, 5, 6, 7, 8, 9 }. PosDigits ::= { 1, 2, 3, 4, 5, 6, 7, 8, 9 }. primitive Problem ::= (s: PosDigits, e: Digits, n: Digits, d: Digits, m: PosDigits, o: Digits, r: Digits, y: Digits). addsUp := p is Problem, (1000*p.s) + (100*p.e) + (10*p.n) + p.d + (1000*p.m) + (100*p.o) + (10*p.r) + p.e = (10000*p.m) + (1000*p.o) + (100*p.n) + (10*p.e) + p.y. sameDigits := val(x,y), val(x,z), y != z. conforms := addsUp & !sameDigits. val ::= (Digits, Digits). val(p.s,0), val(p.e,1), val(p.n,2), val(p.d,3), val(p.m,4), val(p.o,5), val(p.r,6), val(p.y,7) :- p is Problem. } partial model Money of MoreMoney { p is Problem }http://rise4fun.com/Formula/NQueensNQueensdomain NQueens { primitive Size ::= (m: Natural). primitive Queen ::= (x: Natural, y: Natural). WrongNumberOfQueens := Size(m), count(Queen(_,_)) != m. NumberTooBig := Queen(x,_), Size(m), x >= m . NumberTooBig := c is Queen, s is Size, c.y >= s.m . SameRow := a is Queen, b is Queen, a.y = b.y, a != b. SameColumn := a is Queen, b is Queen, a.x = b.x, a != b. SameDiagonal := a is Queen, b is Queen, a != b, a.x - a.y = b.x - b.y. SameDiagonal := a is Queen, b is Queen, a != b, a.x + a.y = b.x + b.y. conforms := !WrongNumberOfQueens & !NumberTooBig & !SameRow & !SameColumn & !SameDiagonal. } partial model Queens16 of NQueens { Size(16) Queen( 0,_) Queen( 1,_) Queen( 2,_) Queen( 3,_) Queen( 4,_) Queen( 5,_) Queen( 6,_) Queen( 7,_) Queen( 8,_) Queen( 9,_) Queen(10,_) Queen(11,_) Queen(12,_) Queen(13,_) Queen(14,_) Queen(15,_) } http://rise4fun.com/Formula/JobShopJobShopdomain JobShop { primitive Machine ::= (id: Integer). primitive Job ::= (id: Integer). [Closed(owner)][Unique(owner, prec -> dur)] primitive Task ::= (owner: Job, prec: Natural, dur: PosInteger). [Closed(task, mach)][Function(task -> start, mach)] primitive Schedule ::= (task: Task, start: Natural, mach: Machine). overlap := s1 is Schedule, s2 is Schedule, s1.task != s2.task, s1.mach = s2.mach, s1.start + s1.task.dur >= s2.start, s1.start <= s2.start. outOfOrder := s1 is Schedule, s2 is Schedule, s1.task.owner = s2.task.owner, s1.start >= s2.start, s1.task.prec < s2.task.prec. tooSlow := s is Schedule, s.start >= 15. conforms := !(overlap | outOfOrder | tooSlow). } partial model MyShop of JobShop { Machine(1) Machine(2) j1 is Job(1) t11 is Task(j1, 1, 10) t12 is Task(j1, 2, 3) j2 is Job(2) t21 is Task(j2, 5, 10) t22 is Task(j2, 10, 6) Schedule(t11,_,_) Schedule(t12,_,_) Schedule(t21,_,_) Schedule(t22,_,_) } http://rise4fun.com/Formula/ConflictGraph2BalancedNetworkConflictGraph2BalancedNetworkdomain Functionality { primitive Task ::= (id: String). [Closed] primitive Conflict ::= (t1: Task, t2: Task). } domain Network { primitive Node ::= (id: String). [Closed(fromNode, toNode)] [Unique(fromNode, toNode -> cap)] primitive Channel ::= (fromNode: Node, toNode: Node, cap: PosInteger). // Ensure each node has 2 input/output channels at max bigFanIn := n is Node, count(Channel(_,n,_)) > 2. bigFanOut := n is Node, count(Channel(n,_,_)) > 2. // Ensure that capacities are balanced mustBal ::= (Node). mustBal(n) :- Channel(_,n,_), Channel(n,_,_). clog := mustBal(n), sum(Channel(_,n,_),2) != sum(Channel(n,_,_),2). conforms := !(bigFanIn | bigFanOut | clog). } domain Mapping extends Functionality, Network { [Closed] [Function(fromTask -> toNode)] primitive Binding ::= (fromTask: Task, toNode: Node). // Check if two conflicting tasks are deployed to the same node inConflict := Binding(t1, n), Binding(t2, n), Conflict(t1, t2). conforms := !inConflict. } partial model Ex of Mapping { t1 is Task("UI") t2 is Task("Voice Recognition") t3 is Task("Network Controller") Conflict(t1, t2) Conflict(t2,t3) n1 is Node("DSP") n2 is Node("GPU") n3 is Node("CPU") c1 is Channel c2 is Channel c3 is Channel c4 is Channel c5 is Channel c6 is Channel c7 is Channel c8 is Channel c9 is Channel } http://rise4fun.com/Formula/EulerEuler/* This Formula specificatin models a problem in graph theory. It tries to find a Eulerian walk within a specified graph. The problem is to find a walk through the graph with the following properties: - all edges in the graph must be used - every edge must be used only once A well known example of this problem is the so called German "Das-ist-das-Haus-vom-Nikolaus" problem, which is modeled within this file. */ domain EulerWay { primitive BaseEdge ::= (x:PosInteger, y:PosInteger). primitive SolutionEdge ::= (pos:PosInteger, x : PosInteger, y : PosInteger). // Make sure we have used all BaseEdge terms in the solution usedBaseEdge ::= (x:PosInteger, y:PosInteger). usedBaseEdge(x,y) :- BaseEdge(x,y), SolutionEdge(_,x,y). usedBaseEdge(x,y) :- BaseEdge(x,y), SolutionEdge(_,y,x). unusedBaseEdge := BaseEdge(x,y), fail usedBaseEdge(x,y). // Make sure our index values are one based and not bigger than the number of base edges indexTooBig := SolutionEdge(x,_,_), x > count(BaseEdge(_,_)). // Make sure that no index is used twice doubleIndex := s1 is SolutionEdge, s2 is SolutionEdge, s1 != s2, s1.pos = s2.pos. // Exclude edges that don't line up //wrongSequence := SolutionEdge(x, Edge(_,b)), SolutionEdge(y, Edge(c,_)), y = x + 1, b != c. wrongSequence := SolutionEdge(pos1,_,y1), SolutionEdge(pos2,x2,_), pos2 = pos1 + 1, y1 != x2. // Avoid using edges twice doubleEdge := SolutionEdge(pos1,x,y), SolutionEdge(pos2,x,y), pos1 != pos2. // Exclude mirrors of already used edges mirrorEdge := SolutionEdge(_,x,y), SolutionEdge(_,y,x). conforms := !unusedBaseEdge & !indexTooBig & !doubleIndex & !wrongSequence & !doubleEdge & !mirrorEdge. } /* Nikolaus graph: 5 / \ 3---4 |\ /| | X | |/ \| 1---2 */ partial model nikolaus2 of EulerWay { BaseEdge(1,2) BaseEdge(1,3) BaseEdge(1,4) BaseEdge(2,4) BaseEdge(2,3) BaseEdge(3,4) BaseEdge(3,5) BaseEdge(4,5) SolutionEdge(1,_,_) SolutionEdge(2,_,_) SolutionEdge(3,_,_) SolutionEdge(4,_,_) SolutionEdge(5,_,_) SolutionEdge(6,_,_) SolutionEdge(7,_,_) SolutionEdge(8,_,_) }http://rise4fun.com/Formula/HierarchicalComponentsHierarchicalComponents// A domain is a unit of structural abstraction. // It contains ADTs and a logic program that defines the structure of the abstraction. // // This specific domain describes the structure of a software component model. domain Software { // The root element of the software component model primitive System ::= (name : String). // Data type constructors with labeled arguments // The owner field refers to either the System or other Components. // // Predefined attribute annotations reduce size of specification: // - The "Closed" attribute requires that all instances of Subsystem // that are used as the second argument of Component, also exists // as a fact in the facts of a model. // - The "Unique" attribute adds a check that for all instances of // Component, there is a unique mapping of names to owners. [Closed(owner)] [Unique(name -> owner)] primitive Component ::= (name : String, owner : Subsystem). [Closed(fromSys, toSys)] primitive Link ::= (name : String, fromSys : Subsystem, toSys : Subsystem). // Arbitrary unions for polymorphism and recursive data types Subsystem ::= System + Component. // The special "conforms" query defines the rules of the abstractions. conforms := count(System(_)) = 1. } // Another independent domain definition, defining a simplified // version of a hardware model. domain Hardware { primitive Node ::= (name : String). [Closed(fromNode, toNode)] primitive Channel ::= (fromNode : Node, toNode : Node). // A derived data type constructor. Type definitions can also omit // the specification of labels for each position. canSend ::= (Node, Node). // Rules generate derived facts based on constraints on other facts. canSend(x, x) :- x is Node. canSend(x, y) :- Channel(x, y). // Fixed-point computation handles recursion canSend(x, z) :- canSend(x, y), canSend(y, z). } // This domain extends the domains Software and Hardware and specifies // additional constraints on how a valid deployment of software components // to hardware nodes must look like. // Extended domains inherit a specification and can add new data types. // Product domains merge type systems and logic programs while conjuncting constraints. domain Partitioning extends Software, Hardware { // Only existing Components may be deployed to existing nodes. Additionally // this annotation requires, that all Components must be deployed. [Closed(sys,node)] [Total(sys)] primitive Deployment ::= (sys : Component, node : Node). // Negation-as-failure allows a rule to check for the absence of a fact. cannotSend := Deployment(c1, n1), Deployment(c2, n2), Link(_, c1, c2), fail canSend(n1, n2). // Inherited constraints of Software and Hardware are implicitly added // to the conforms query of this domain. conforms := !cannotSend. } // Although the partial model contains no specific unknowns, some terms are missing // for a valid model satisfying all constraints. // FORMULA automatically adds the required number of instances for the // type Deployment prior to model finding. partial model PartitioningProblem of Partitioning { root is System("root") c1 is Component("comp1", root) c2 is Component("comp2", root) Link("connect", c1, c2) n1 is Node("node1") n2 is Node("node2") Channel(n1,n2) } http://rise4fun.com/Formula/GraphColoringGraphColoringdomain GraphColoring { Color ::= { c0, c1, c2, c3, c4, c5 }. primitive Vertex ::= (id: Integer). [Closed] primitive Edge ::= (v1: Vertex, v2: Vertex). [Closed(v)] primitive Coloring ::= (v: Vertex, c: Color). badColoring := Edge(u, w), Coloring(u, c), Coloring(w, c), u != w. conforms := !badColoring. } partial model RandomGraph of GraphColoring { v0 is Vertex(0) v1 is Vertex(1) v2 is Vertex(2) v3 is Vertex(3) v4 is Vertex(4) v5 is Vertex(5) v6 is Vertex(6) v7 is Vertex(7) v8 is Vertex(8) v9 is Vertex(9) v10 is Vertex(10) v11 is Vertex(11) v12 is Vertex(12) v13 is Vertex(13) v14 is Vertex(14) v15 is Vertex(15) v16 is Vertex(16) v17 is Vertex(17) v18 is Vertex(18) v19 is Vertex(19) v20 is Vertex(20) v21 is Vertex(21) v22 is Vertex(22) v23 is Vertex(23) v24 is Vertex(24) Edge(v0, v1) Edge(v0, v5) Edge(v0, v6) Edge(v0, v7) Edge(v0, v10) Edge(v0, v12) Edge(v0, v17) Edge(v0, v20) Edge(v0, v24) Edge(v1, v3) Edge(v1, v4) Edge(v1, v7) Edge(v1, v9) Edge(v1, v10) Edge(v1, v12) Edge(v1, v13) Edge(v1, v15) Edge(v1, v16) Edge(v1, v17) Edge(v1, v19) Edge(v1, v21) Edge(v2, v4) Edge(v2, v9) Edge(v2, v12) Edge(v2, v14) Edge(v2, v16) Edge(v2, v17) Edge(v2, v18) Edge(v2, v19) Edge(v2, v21) Edge(v2, v22) Edge(v2, v23) Edge(v3, v6) Edge(v3, v12) Edge(v3, v13) Edge(v3, v16) Edge(v3, v21) Edge(v3, v23) Edge(v3, v24) Edge(v4, v6) Edge(v4, v7) Edge(v4, v8) Edge(v4, v10) Edge(v4, v14) Edge(v4, v17) Edge(v4, v18) Edge(v4, v20) Edge(v4, v22) Edge(v5, v6) Edge(v5, v8) Edge(v5, v9) Edge(v5, v10) Edge(v5, v13) Edge(v5, v15) Edge(v5, v16) Edge(v5, v17) Edge(v5, v18) Edge(v5, v19) Edge(v5, v24) Edge(v6, v7) Edge(v6, v8) Edge(v6, v9) Edge(v6, v12) Edge(v6, v14) Edge(v6, v16) Edge(v6, v17) Edge(v6, v18) Edge(v6, v20) Edge(v6, v21) Edge(v6, v22) Edge(v7, v8) Edge(v7, v13) Edge(v7, v15) Edge(v7, v16) Edge(v7, v19) Edge(v7, v20) Edge(v7, v22) Edge(v7, v23) Edge(v7, v24) Edge(v8, v11) Edge(v8, v18) Edge(v8, v20) Edge(v9, v13) Edge(v9, v14) Edge(v9, v15) Edge(v9, v16) Edge(v9, v17) Edge(v9, v18) Edge(v9, v19) Edge(v9, v20) Edge(v9, v21) Edge(v9, v22) Edge(v9, v23) Edge(v10, v13) Edge(v10, v15) Edge(v10, v17) Edge(v10, v18) Edge(v10, v19) Edge(v10, v20) Edge(v11, v12) Edge(v11, v15) Edge(v11, v17) Edge(v11, v19) Edge(v11, v22) Edge(v11, v24) Edge(v12, v13) Edge(v12, v15) Edge(v12, v16) Edge(v12, v19) Edge(v12, v21) Edge(v12, v24) Edge(v13, v14) Edge(v13, v15) Edge(v13, v16) Edge(v13, v17) Edge(v13, v18) Edge(v13, v21) Edge(v13, v22) Edge(v13, v23) Edge(v13, v24) Edge(v14, v15) Edge(v14, v16) Edge(v14, v22) Edge(v15, v16) Edge(v15, v17) Edge(v15, v20) Edge(v15, v21) Edge(v16, v17) Edge(v16, v19) Edge(v16, v21) Edge(v17, v19) Edge(v17, v22) Edge(v17, v23) Edge(v17, v24) Edge(v18, v19) Edge(v18, v21) Edge(v18, v24) Edge(v19, v22) Edge(v19, v24) Edge(v20, v21) Edge(v20, v23) Edge(v20, v24) Coloring(v0, _) Coloring(v1, _) Coloring(v2, _) Coloring(v3, _) Coloring(v4, _) Coloring(v5, _) Coloring(v6, _) Coloring(v7, _) Coloring(v8, _) Coloring(v9, _) Coloring(v10, _) Coloring(v11, _) Coloring(v12, _) Coloring(v13, _) Coloring(v14, _) Coloring(v15, _) Coloring(v16, _) Coloring(v17, _) Coloring(v18, _) Coloring(v19, _) Coloring(v20, _) Coloring(v21, _) Coloring(v22, _) Coloring(v23, _) Coloring(v24, _) }