Compare commits

...

2 Commits

  1. 2
      Computergrafiek Project/graphics_project_21-22-Danacus
  2. BIN
      Digitale elektronica en processoren/2022-03-25_11-07-29_sheet.rnote
  3. BIN
      Internet Infrastructure/ii-zones.rnote
  4. 2
      MAS/PacketWorld
  5. BIN
      MCS/2022-03-18_14-01-03_sheet.rnote
  6. 103
      MCS/idp/project/elevator.idp
  7. 2
      Swarch/sa-project

@ -1 +1 @@
Subproject commit 4be5abadf349c6f7293f9c990ccc941c4b897cc9
Subproject commit e57549f13fe7787d572adcf07d70ac4dd8f1dd40

@ -1 +1 @@
Subproject commit 3e1751cd809e3b62707694d5173fc98130017b91
Subproject commit 0e39f9bc815198f7dfbb81ac33615cb4bea60197

@ -29,15 +29,35 @@ LTCvocabulary V_student {
extern vocabulary V_fixed
type Direction constructed from {Up, Down, None} // Direction in which the elevator is moving
<<<<<<< HEAD
=======
type RelPos constructed from {Above, Below} // Location of a request relative to the elevator
// Actions
Move(Time, Direction)
>>>>>>> 182effcf4c02a91baa62092c6de0cae1a57db72e
// Fluents
ElDirection(Time): Direction
I_ElDirection: Direction
C_ElDirection(Time, Direction)
<<<<<<< HEAD
I_ElPosition: Floor
C_ElPosition(Time, Floor)
I_UnansweredRequest(Floor)
AddRequest(Time, Floor)
AnswerRequest(Time, Floor)
I_ElDoorState: DoorState
C_ElDoorState(Time, DoorState)
// Helpers
CanMove(Time)
HasRequest(Time, Direction)
ClosestRequest(Time, Direction, Floor)
=======
I_ElPosition: Floor
C_ElPosition(Time, Floor)
@ -53,6 +73,7 @@ LTCvocabulary V_student {
CanMove(Time)
HasRequest(Time, RelPos)
ClosestRequest(Time, RelPos, Floor)
>>>>>>> 182effcf4c02a91baa62092c6de0cae1a57db72e
}
// TIME THEORY
@ -78,22 +99,46 @@ Theory T_student:V_student {
I_ElDirection = None.
I_ElPosition = 0.
<<<<<<< HEAD
=======
{
!t [Time]: Move(t, Down) <- (C_ElDirection(t, Down) | ElDirection(t) = Down) & CanMove(t) & HasRequest(t, Below).
!t [Time]: Move(t, Up) <- (C_ElDirection(t, Up) | ElDirection(t) = Up) & CanMove(t) & HasRequest(t, Above).
}
>>>>>>> 182effcf4c02a91baa62092c6de0cae1a57db72e
/***************\
* DEFINITIONS *
\***************/
{ // CanMove definition, true iff we are allowed to move
// We are allowed to move when the doors are closed and not changing
<<<<<<< HEAD
!t [Time]: CanMove(t) <- ~?s [DoorState]: C_ElDoorState(t, s) & ElDoorState(t) = Closed.
=======
!t [Time]: CanMove(t) <- (~?s [DoorState]: C_ElDoorState(t, s)) & ElDoorState(t) = Closed.
>>>>>>> 182effcf4c02a91baa62092c6de0cae1a57db72e
}
{
// HasRequest definition, true iff there is an unanswered request in the given direction
<<<<<<< HEAD
// It needed to be hacked to also count new request causes as unanswered requests,
// even though UnansweredRequest would only be true at the next time step.
!t [Time]: HasRequest(t, Up) <-
?f [Floor]: (AddRequest(t, f) | UnansweredRequest(t, f)) & ElPosition(t) < f.
!t [Time]: HasRequest(t, Down) <-
?f [Floor]: (AddRequest(t, f) | UnansweredRequest(t, f)) & ElPosition(t) > f.
}
{
!t [Time] f [Floor]: ClosestRequest(t, Up, f) <- ElPosition(t) < f
& (AddRequest(t, f) | UnansweredRequest(t, f))
& !f2 [Floor]: (UnansweredRequest(t, f)) & f ~= f2 => f2 < f.
!t [Time] f [Floor]: ClosestRequest(t, Down, f) <- ElPosition(t) > f
& (AddRequest(t, f) | UnansweredRequest(t, f))
& !f2 [Floor]: (UnansweredRequest(t, f)) & f ~= f2 => f2 > f.
=======
!t [Time]: HasRequest(t, Above) <-
?f [Floor]: UnansweredRequest(t, f) & ElPosition(t) < f.
!t [Time]: HasRequest(t, Below) <-
@ -107,6 +152,7 @@ Theory T_student:V_student {
!t [Time] f [Floor]: ClosestRequest(t, Below, f) <-
ElPosition(t) > f & UnansweredRequest(t, f)
& !f2 [Floor]: UnansweredRequest(t, f2) & f ~= f2 => f2 > f.
>>>>>>> 182effcf4c02a91baa62092c6de0cae1a57db72e
}
/**************************\
@ -144,6 +190,29 @@ Theory T_student:V_student {
{
/// Direction changes ///
<<<<<<< HEAD
// If there is no request above you but there is one below you,
// you should already have changed the direction to Down.
!t [Time]: C_ElDirection(t, Down) <- ~HasRequest(t, Up) & HasRequest(t, Down).
!t [Time] fd [Floor] fu [Floor]: C_ElDirection(t, Down) <-
HasRequest(t, Up) & HasRequest(t, Down)
& (C_ElDirection(t, None) | ElDirection(t) = None)
& ClosestRequest(t, Down, fd) & ClosestRequest(t, Up, fu)
& ElPosition(t) - fd < fu - ElPosition(t).
// If there is no request below you but there is one above you,
// you should already have changed the direction to Up.
!t [Time]: C_ElDirection(t, Up) <- ~HasRequest(t, Down) & HasRequest(t, Up).
!t [Time] fd [Floor] fu [Floor]: C_ElDirection(t, Up) <-
HasRequest(t, Up) & HasRequest(t, Down)
& (C_ElDirection(t, None) | ElDirection(t) = None)
& ClosestRequest(t, Down, fd) & ClosestRequest(t, Up, fu)
& ElPosition(t) - fd >= fu - ElPosition(t).
!t [Time]: C_ElDirection(t, None) <- ~HasRequest(t, Down) & ~HasRequest(t, Up).
=======
// If there is no request above you but there is one below you, change the direction to Down.
!t [Time]: C_ElDirection(t, Down) <- HasRequest(t, Below) & ~HasRequest(t, Above).
@ -162,10 +231,18 @@ Theory T_student:V_student {
ElDirection(t) = None
& ClosestRequest(t, Below, fd) & ClosestRequest(t, Above, fu)
& ElPosition(t) - fd < fu - ElPosition(t).
>>>>>>> 182effcf4c02a91baa62092c6de0cae1a57db72e
/// Movement ///
<<<<<<< HEAD
// Move up if we are going up and we can move
!t [Time]: C_ElPosition(t, ElPosition(t) + 1) <- ElDirection(t) = Up & CanMove(t) & HasRequest(t, Up).
// Move down if we are going down and we can move
!t [Time]: C_ElPosition(t, ElPosition(t) - 1) <- ElDirection(t) = Down & CanMove(t) & HasRequest(t, Down).
=======
// Uses ramifications to allow the elevator to start moving while the direction changes
// instead of having to wait until the direction has changed.
@ -178,6 +255,7 @@ Theory T_student:V_student {
!t [Time]: C_ElPosition(t, ElPosition(t) - 1) <-
Move(t, Down).
//(C_ElDirection(t, Down) | ElDirection(t) = Down) & CanMove(t) & HasRequest(t, Below).
>>>>>>> 182effcf4c02a91baa62092c6de0cae1a57db72e
/// Door opening and closing ///
@ -197,6 +275,26 @@ Theory T_student:V_student {
// Answer a request when the doors are open and we are at the floor of the request
!t [Time] f [Floor]: AnswerRequest(t, f) <- ElDoorState(t) = Open & ElPosition(t) = f.
}
<<<<<<< HEAD
}
// If elevator moves the doors are closed!
theory move_inv : V_student {
!t [Time]: ?f [Floor]: C_ElPosition(t, f) => ElDoorState(Next(t)) = Closed.
}
// Doors are never open if there is no call waiting on that floor!
theory door_inv : V_student {
!t [Time]: ElDoorState(t) = Open => UnansweredRequest(t, ElPosition(t)).
}
Structure S_Inv : V_student {
Time = { 0..20 }
Floor = { 0..5 }
Start = 0
}
=======
}
// If elevator moves the doors are closed!
@ -215,6 +313,7 @@ Structure S_Inv : V_student {
Start = 0
}
>>>>>>> 182effcf4c02a91baa62092c6de0cae1a57db72e
procedure proveInvariants() {
print(isinvariant(T_student, move_inv, S_Inv))
print(isinvariant(T_student, door_inv, S_Inv))
@ -228,7 +327,11 @@ procedure main() {
local CompleteTheory = merge(T_fixed, T_student)
// Change the structure name to try other structures (check the included file "structures.idp" for available provided structures, and feel free to add additional structures)
<<<<<<< HEAD
model = onemodel(CompleteTheory, S9)
=======
model = onemodel(CompleteTheory, S11)
>>>>>>> 182effcf4c02a91baa62092c6de0cae1a57db72e
//explainunsat(CompleteTheory, S8)
// Printing model

@ -1 +1 @@
Subproject commit 917c21e812bfef334e269747ed105e1dd98352c5
Subproject commit 282bea1af0f618be79562dcaa7526a8fcbea70a2
Loading…
Cancel
Save