Small improvements

cwi-swat · Jul 23, 2018 · a63ce88 · a63ce88
1 parent b5da3f0
commit a63ce88
Show file tree

Hide file tree

Showing 4 changed files with 6 additions and 6 deletions.
diff --git a/examples/int/account.alle b/examples/int/account.alle
@@ -20,8 +20,6 @@ Account[aId] ⊆ ((InitialState[sId as from] ⨝ *<from,to>ordering)[to][to as s
 
 ∀ s ∈ State ∖ (InitialState ⨝ State) |  some (s where amount > 0 && amount < 11)
 
-//∀ s ∈ (State[sId] ∖ InitialState) ⨝ State | some (s where amount > 0 && amount < 11)
-
 // Initial state
 some ((InitialState ⨝ accountInState ⨝ Account) where balance = 0)
 

diff --git a/examples/int/ropebridge.alle b/examples/int/ropebridge.alle
@@ -78,7 +78,7 @@ Traveller[tId] ⊆ (last ⨝ posOfTrav ⨝ far)[tId]
   )   
 
 // check that it is impossible (unsatisfiable) for all the travellers to cross the bridge in less then 17 minutes  
-//some order[sum(timeSpend) as totalTimeSpend] where totalTimeSpend < 17
+some order[sum(timeSpend) as totalTimeSpend] where totalTimeSpend = 17
 
 // minimize the time that it takes the travellers to cross the bridge  
-objectives: minimize order[sum(timeSpend)]
+//objectives: minimize order[sum(timeSpend)]
diff --git a/examples/optimization/rushhour.alle b/examples/optimization/rushhour.alle
@@ -54,7 +54,8 @@ State ⨯ Vehicle[vId] ⊆ posInState[sId,vId]
 ∃ s ∈ State | some (posInState ⨝ s ⨝ RedCar) where pos = 4
 
 // only 1 vehicle can move between different states
-∀ o ∈ ordering | let s = o[cur][cur as sId], s' = o[next][next as sId], curPos = (posInState ⨝ s)[vId,pos], nxtPos = (posInState ⨝ s')[vId,pos] | one nxtPos ∖ curPos
+∀ o ∈ ordering | let s = o[cur][cur as sId], s' = o[next][next as sId], curPos = (posInState ⨝ s)[vId,pos], nxtPos = (posInState ⨝ s')[vId,pos] | 
+  one nxtPos ∖ curPos
 
 // two horizontal vehicles in the same row should never overlap
 ∀ s ∈ State, h1 ∈ Horizontal ⨝ Vehicle ⨝ posInState ⨝ s, h2 ∈ ((Horizontal ⨝ Vehicle ⨝ posInState ⨝ s) ∖ h1)[vId as vId', sId as sId', length as length', row as row', pos as pos'] | 

diff --git a/examples/relational/thief.alle b/examples/relational/thief.alle
@@ -26,4 +26,5 @@ one thief
 // Their class teacher now comes in. She says: "three of these boys always tell the truth and two always lie." 
 // The class teacher is telling the truth.
 let students = matthew ∪ peter ∪ jack ∪ arnold ∪ carl | 
-  ∃ s1 ∈ students, s2 ∈ students ∖ s1 | (s1 ∪ s2) = liar
+  ∃ s1 ∈ students, s2 ∈ students ∖ s1 | (s1 ∪ s2) = liar
+//some liar[count() as nr] where nr = 2