Skip to content
Snippets Groups Projects
Commit c70cb91d authored by Pascal Huesing's avatar Pascal Huesing
Browse files

Lösungen hochgeladen.

parent fd14a18f
Branches master
No related tags found
No related merge requests found
......@@ -3,6 +3,7 @@
/Solutions/Clock/JumpyClock.toolbox/
/Solutions/Clock/Clock.toolbox/
/Solutions/Clock/states/
/Solutions/CoffeeCan/CoffeeCan.toolbox/
/Solutions/Hanoi/Hanoi.toolbox/
......@@ -12,4 +13,4 @@
/Specs/DieHard/DieHard.toolbox/
/Specs/Hanoi/Hanoi.toolbox/
/Specs/SimpleProgram/SimpleProgram.toolbox/
/Specs/TCommit/TCommit.toolbox/
\ No newline at end of file
/Specs/TCommit/TCommit.toolbox/
INIT Init
NEXT Next
INVARIANT TypeOK
PROPERTY TimeOK
\ No newline at end of file
------------------------------- MODULE Clock -------------------------------
EXTENDS Naturals
VARIABLES hour, minute, second
vars == <<hour, minute, second>>
Init ==
/\ hour = 0
/\ minute = 0
/\ second = 0
TypeOK == /\ hour >= 0
/\ hour <= 23
/\ minute >= 0
/\ minute <= 59
/\ second >= 0
/\ second <= 59
TotalSeconds(h, m, s) ==
s + (m*60) + (h*60*60)
Tick ==
/\ hour' = IF second = 59 /\ minute = 59
THEN IF hour = 23
THEN 0
ELSE hour + 1
ELSE hour
/\ minute' = IF second = 59
THEN IF minute = 59
THEN 0
ELSE minute + 1
ELSE minute
/\ second' = IF second = 59
THEN 0
ELSE second + 1
TimeOK == [][(hour # 23 \/ minute # 59 \/ second # 59) => TotalSeconds(hour', minute', second') = TotalSeconds(hour, minute, second) + 1]_vars
Next == /\ Tick
Spec == Init /\ [][Next]_<<hour, minute, second>>
=============================================================================
\* Modification History
\* Last modified Tue May 23 20:10:49 GMT 2023 by ?
\* Last modified Tue May 23 20:28:09 GMT 2023 by pascal
\* Created Tue May 23 20:13:26 GMT 2023 by pascal
\ No newline at end of file
INIT Init
NEXT Next
INVARIANT TypeOK
PROPERTY TimeOK
\ No newline at end of file
----------------------------- MODULE JumpyClock -----------------------------
EXTENDS Naturals
VARIABLES hour, minute, second
vars == <<hour, minute, second>>
Init ==
/\ hour = 0
/\ minute = 0
/\ second = 0
TypeOK == /\ hour >= 0
/\ hour <= 23
/\ minute >= 0
/\ minute <= 59
/\ second >= 0
/\ second <= 59
TotalSeconds(h, m, s) ==
s + (m*60) + (h*60*60)
IsInFuture(h, m, s) ==
TotalSeconds(h, m, s) > TotalSeconds(hour, minute, second)
Jump ==
/\ \E next_hour \in 0..23 :
\E next_minute \in 0..59:
\E next_second \in 0..59:
/\ IsInFuture(next_hour, next_minute, next_second)
/\ hour' = next_hour
/\ minute' = next_minute
/\ second' = next_second
Tick ==
/\ hour' = IF second = 59 /\ minute = 59
THEN IF hour = 23
THEN 0
ELSE hour + 1
ELSE hour
/\ minute' = IF second = 59
THEN IF minute = 59
THEN 0
ELSE minute + 1
ELSE minute
/\ second' = IF second = 59
THEN 0
ELSE second + 1
TimeOK == [][(hour # 23 \/ minute # 59 \/ second # 59) => TotalSeconds(hour', minute', second') = TotalSeconds(hour, minute, second) + 1]_vars
Next == Jump \/ Tick
Spec == Init /\ [][Next]_<<hour, minute, second>>
=============================================================================
\* Modification History
\* Last modified Tue May 23 19:49:47 GMT 2023 by ?
\* Last modified Tue May 23 20:28:09 GMT 2023 by pascal
\* Created Tue May 23 20:13:26 GMT 2023 by pascal
\ No newline at end of file
CONSTANTS
MaxBeanCount = 1000
SPECIFICATION
Spec
PROPERTY
EventuallyTerminates
MonotonicDecrease
LoopInvariant
TerminationHypothesis
INVARIANTS
TypeInvariant
---------------------------- MODULE CoffeeCan -------------------------------
EXTENDS Naturals
CONSTANT MaxBeanCount
ASSUME MaxBeanCount \in Nat /\ MaxBeanCount >= 1
VARIABLES can
Can == [black : 0..MaxBeanCount, white : 0..MaxBeanCount]
TypeInvariant == can \in Can
Init == can \in {c \in Can : c.black + c.white \in 1..MaxBeanCount}
BeanCount == can.black + can.white
PickSameColorBlack ==
/\ BeanCount > 1
/\ can.black >= 2
(* Aktueller Wert von schwarzen Bohnen wird um 1 reduziert. *)
/\ can' = [can EXCEPT !.black = @ - 1]
PickSameColorWhite ==
/\ BeanCount > 1
/\ can.white >= 2
(* Aktueller Wert von schwarzen Bohnen wird um 1 erhöht und der Wert von weißen Bohnen um 2 reduziert. *)
/\ can' = [can EXCEPT !.black = @ + 1, !.white = @ - 2]
PickDifferentColor ==
/\ BeanCount > 1
/\ can.black >= 1
/\ can.white >= 1
(* Aktueller Wert von schwarzen Bohnen wird um 1 verringert. *)
/\ can' = [can EXCEPT !.black = @ - 1]
Termination ==
/\ BeanCount = 1
/\ UNCHANGED can
Next ==
\/ PickSameColorWhite
\/ PickSameColorBlack
\/ PickDifferentColor
\/ Termination
(* Invariante, die besagt, dass die Anzahl an Bohnen in jedem Zustand des Systems monoton abnimmt. *)
MonotonicDecrease == [][BeanCount' < BeanCount]_can
(* Invariante, die besagt, die weißen Bohnen immer gerade oder ungerade sein müssen *)
LoopInvariant == [][can.white % 2 = 0 <=> can'.white % 2 = 0]_can
(* Invariante, die besagt, dass die Aktion "Terminierung" irgendwann ausgeführt werden muss. *)
EventuallyTerminates == <>(ENABLED Termination)
(* Stelle eine Hypothese zur Terminierung des Systems auf, abhängig von der Parität der weißen Bohnen in der Kanne. *)
TerminationHypothesis ==
IF can.white % 2 = 0
THEN <>(can.black = 1 /\ can.white = 0)
ELSE <>(can.black = 0 /\ can.white = 1)
Spec ==
/\ Init
/\ [][Next]_can
/\ WF_can(Next)
THEOREM Spec =>
/\ TypeInvariant
/\ MonotonicDecrease
/\ EventuallyTerminates
/\ LoopInvariant
/\ TerminationHypothesis
=============================================================================
\* Modification History
\* Last modified Tue May 23 18:58:17 GMT 2023 by ?
\* Last modified Tue May 23 20:28:09 GMT 2023 by pascal
\* Created Tue May 23 20:13:26 GMT 2023 by pascal
\ No newline at end of file
import tlc2.value.IntValue;
public class Bits {
public static IntValue And(IntValue x, IntValue y, IntValue n, IntValue m) {
return IntValue.gen(x.val & y.val);
}
}
-------------------------------- MODULE Bits --------------------------------
LOCAL INSTANCE Integers
RECURSIVE And(_,_,_,_)
LOCAL And(x,y,n,m) == LET exp == 2^n
IN IF m = 0
THEN 0
ELSE exp * ((x \div exp) % 2) * ((y \div exp) % 2)
+ And(x,y,n+1,m \div 2)
x & y == And(x, y, 0, x)
=============================================================================
\* Modification History
\* Last modified Tue May 23 20:28:09 GMT 2023 by pascal
\* Created Tue May 23 20:13:26 GMT 2023 by pascal
INIT Init
NEXT Next
CONSTANTS
D = 3
N = 3
SPECIFICATION
Spec
INVARIANTS
TypeOK
NotSolved
------------------------------- MODULE Hanoi -------------------------------
EXTENDS Naturals, Bits, FiniteSets, TLC
(* Ueberprueft, ob eine gegebene Zahl i eine Potenz von zwei ist. *)
PowerOfTwo(i) == i & (i-1) = 0
(* Erstellt die Menge aller Zahlen von 1 bis 2^n-1, die Potenzen von zwei sind. *)
SetOfPowerOfTwo(n) == {x \in 1..(2^n-1): PowerOfTwo(x)}
(* Berechnet die Summe aller Werte in einer gegebenen Funktion f. *)
Sum(f) == LET DSum[S \in SUBSET DOMAIN f] ==
LET elt == CHOOSE e \in S : TRUE
IN IF S = {} THEN 0
ELSE f[elt] + DSum[S \ {elt}]
IN DSum[DOMAIN f]
(* D = Anzahl der Scheiben, N = Anzahl der Tuerme. *)
CONSTANT D, N
(* Towers ist eine Funktion die jeden Tower eine Anzahl von Scheiben zuordnet *)
VARIABLES towers
vars == <<towers>>
(* Invariante, die prueft ob die Anzahl der Scheiben ueber alle Tower noch gleich ist *)
Inv == Sum(towers) = 2^D - 1
(* Invariante, die prueft ob jeder Tower noch gueltige Werte hat *)
TypeOK == /\ \A i \in DOMAIN towers : /\ towers[i] \in Nat
/\ towers[i] < 2^D
(* Der erste Turm hat alle Scheiben, alle anderen Tuerme haben keine Scheiben *)
Init == /\ towers = [i \in 1..N |-> IF i = 1 THEN 2^D - 1 ELSE 0]
(* Der Turm hat keine Scheiben wenn er auf 0 abgebildet wird. *)
IsEmptyTower(tower) == tower = 0
(* Wenn das Bit fuer die Disk auf den Tower ist ergibt die Verundung die selbe Zahl. *)
IsOnTower(tower, disk) == /\ tower & disk = disk
(* (disk - 1) invertiert alle Bits hinter dem LSB und verundet die mit dem Tower. *)
IsSmallestDisk(tower, disk) == /\ IsOnTower(tower, disk)
/\ tower & (disk - 1) = 0
(* Eine Disk darf vom Tower herunterbewegt werden, wenn es die smallest disk ist und auf dem Tower ist *)
CanMoveOff(tower, disk) == /\ IsOnTower(tower, disk)
/\ IsSmallestDisk(tower, disk)
(* Eine Disk darf nur auf einen Tower gesetzt werden, wenn es die smallest disk ist oder der Tower leer ist. *)
CanMoveTo(tower, disk) == \/ tower & (disk - 1) = 0
\/ IsEmptyTower(tower)
(* Verwendet die verschiedenen Move Methoden um die Move Aktion zu modellieren. *)
Move(from, to, disk) == /\ CanMoveOff(towers[from], disk)
/\ CanMoveTo(towers[to], disk)
/\ towers' = [towers EXCEPT ![from] = towers[from] - disk,
![to] = towers[to] + disk]
(* Es wird irgendeine Scheibe ausgewaehlt, sodass gilt wenn man zwei unterschiedliche Tuerme auswaehlt, dass diese Scheibe mittels move verschoden werden kann. *)
Next == \E d \in SetOfPowerOfTwo(D): \E idx1, idx2 \in DOMAIN towers:
/\ idx1 # idx2
/\ Move(idx1, idx2, d)
Spec == Init /\ [][Next]_vars
(* Invariante, die prueft, ob das Problem schon geloest ist. *)
NotSolved == towers[N] # 2^D - 1
=============================================================================
\* Modification History
\* Last modified Tue May 23 20:28:09 GMT 2023 by pascal
\* Created Tue May 23 20:13:26 GMT 2023 by pascal
\ No newline at end of file
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment