master
Daan Vanoverloop 2 months ago
parent db403d3f74
commit 6e1e945814
  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. 168
      MCS/idp/project/elevator.idp
  7. 10
      MCS/idp/project/structures.idp
  8. 2
      Swarch/sa-project

@ -1 +1 @@
Subproject commit bcf2b41b30670db5c7c4d49819346386bc4baa0d
Subproject commit e57549f13fe7787d572adcf07d70ac4dd8f1dd40

@ -1 +1 @@
Subproject commit 809f66281b7622aee0e0e9eda36b4a5054107914
Subproject commit 0e39f9bc815198f7dfbb81ac33615cb4bea60197

@ -28,13 +28,27 @@ LTCvocabulary V_fixed {
LTCvocabulary V_student {
extern vocabulary V_fixed
type Direction constructed from {Up, Down} // Direction in which the elevator is moving
type Direction constructed from {Up, Down, None} // Direction in which the elevator is moving
// Fluents
ElDirection(Time): Direction
I_ElDirection: Direction
C_ElDirection(Time, Direction)
// Causalities
C_ElDirection
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)
}
// TIME THEORY
@ -51,24 +65,168 @@ Theory T_fixed : V_student {
// STUDENT THEORY
// Here you should model the dynamic elevator system
Theory T_student:V_student {
/*****************\
* INITIAL STATE *
\*****************/
!f [Floor]: ~I_UnansweredRequest(f). // Initially there are not requests
I_ElDoorState = Closed.
I_ElDirection = None.
I_ElPosition = 0.
/***************\
* DEFINITIONS *
\***************/
{ // CanMove definition, true iff we are allowed to move
// We are allowed to move when the doors are closed and not changing
!t [Time]: CanMove(t) <- ~?s [DoorState]: C_ElDoorState(t, s) & ElDoorState(t) = Closed.
}
{
// HasRequest definition, true iff there is an unanswered request in the given direction
// 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.
}
/**************************\
* SUCCESSOR STATE AXIOMS *
\**************************/
{ // ElPosition
ElPosition(Start) = I_ElPosition <- .
!t [Time] f [Floor]: ElPosition(Next(t)) = f <- C_ElPosition(t, f).
!t [Time] f [Floor]: ElPosition(Next(t)) = ElPosition(t) <- ~?f2 [Floor]: C_ElPosition(t, f2).
}
{ // ElDirection
ElDirection(Start) = I_ElDirection <- .
!t [Time] d [Direction]: ElDirection(Next(t)) = d <- C_ElDirection(t, d).
!t [Time] d [Direction]: ElDirection(Next(t)) = ElDirection(t) <- ~?d2 [Direction]: C_ElDirection(t, d2).
}
{ // ElDoorState
ElDoorState(Start) = I_ElDoorState <- .
!t [Time] s [DoorState]: ElDoorState(Next(t)) = s <- C_ElDoorState(t, s).
!t [Time] s [DoorState]: ElDoorState(Next(t)) = ElDoorState(t) <- ~?s2 [DoorState]: C_ElDoorState(t, s2).
}
{ // UnansweredRequest
!f [Floor]: UnansweredRequest(Start, f) <- I_UnansweredRequest(f).
!t [Time] f [Floor]: UnansweredRequest(Next(t), f) <- AddRequest(t, f).
!t [Time] f [Floor]: UnansweredRequest(Next(t), f) <- UnansweredRequest(t, f) & ~AnswerRequest(t, f).
}
/**********\
* CAUSES *
\**********/
{
/// Direction changes ///
// 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).
/// Movement ///
// 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).
/// Door opening and closing ///
// Open the door when there is an unanswered request and the door is still closed
!t [Time]: C_ElDoorState(t, Open) <- UnansweredRequest(t, ElPosition(t)) & ElDoorState(t) = Closed.
// Always close the door when it is open, it will never be open for longer than 1 time interval
!t [Time]: C_ElDoorState(t, Closed) <- ElDoorState(t) = Open.
/// Requests ///
// Add an unanswered request when we make one
!t [Time] f [Floor]: AddRequest(t, f) <- MakeRequest(t, f).
// 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.
}
}
// 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
}
procedure proveInvariants() {
print(isinvariant(T_student, move_inv, S_Inv))
print(isinvariant(T_student, door_inv, S_Inv))
}
// MAIN PROCEDURE
// If you have to change the main procedure for debugging purposes, be careful and restore it back once you finish debugging.
procedure main() {
proveInvariants()
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)
model = onemodel(CompleteTheory, S1)
model = onemodel(CompleteTheory, S9)
//explainunsat(CompleteTheory, S8)
// Printing model
print(model)
// Visualization
initVisualization()
visualizeElevator(model)
}
// File responsible for visualization

@ -55,7 +55,17 @@ Structure S7:V_student {
// Feel free to add your own structures here:
Structure S8:V_student {
Time = {0..2}
Floor = {0..2}
MakeRequest = {0, 1}
}
Structure S9:V_student {
Time = {0..20}
Floor = {0..7}
MakeRequest = {0, 4; 7, 3; 7, 6}
}

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