From 3484c38771329b022c0ab1bfa0fff68bbbf65407 Mon Sep 17 00:00:00 2001
From: Juan Lauer Garrido <juan.lauer_garrido@student.reutlingen-university.de>
Date: Tue, 14 Jun 2022 08:48:46 +0200
Subject: [PATCH] Final Push
---
ErzeugerVerbraucher/src/Buffer.java | 3 +++
ErzeugerVerbraucher/src/Car.java | 3 +++
ErzeugerVerbraucher/src/Consumer.java | 5 ++++-
ErzeugerVerbraucher/src/Producer.java | 2 +-
4 files changed, 11 insertions(+), 2 deletions(-)
diff --git a/ErzeugerVerbraucher/src/Buffer.java b/ErzeugerVerbraucher/src/Buffer.java
index 3ab26b2..43c1f63 100644
--- a/ErzeugerVerbraucher/src/Buffer.java
+++ b/ErzeugerVerbraucher/src/Buffer.java
@@ -1,6 +1,7 @@
import java.util.concurrent.atomic.AtomicInteger;
import java.util.concurrent.atomic.AtomicReferenceArray;
+
/**
* A generic and atomically safe Buffer data structure for holding values important in multithreaded use cases.
* @param <T> The type of item to hold within the Buffer
@@ -18,6 +19,8 @@ public class Buffer<T> {
this.items = new AtomicReferenceArray<>(size);
this.itemCount = new AtomicInteger(0);
this.size = size;
+
+ assert this.size >= 0 : "Size must be greater than 0";
}
/**
diff --git a/ErzeugerVerbraucher/src/Car.java b/ErzeugerVerbraucher/src/Car.java
index 5cad0e4..2eee4fc 100644
--- a/ErzeugerVerbraucher/src/Car.java
+++ b/ErzeugerVerbraucher/src/Car.java
@@ -1,2 +1,5 @@
public class Car {
+ /**
+ * Class Car
+ */
}
diff --git a/ErzeugerVerbraucher/src/Consumer.java b/ErzeugerVerbraucher/src/Consumer.java
index 4cf398c..e3e04aa 100644
--- a/ErzeugerVerbraucher/src/Consumer.java
+++ b/ErzeugerVerbraucher/src/Consumer.java
@@ -14,6 +14,9 @@ public class Consumer implements Runnable {
* @param asleep Boolean for Status
* @param wakeCall Boolean for Status
*/
+ /**
+ "@Requires"({"buffer!=null","interval > 0","asleep!=null","wakeCall!=null", })
+ */
public Consumer(Buffer<Car> buffer, int interval, AtomicBoolean asleep, AtomicBoolean wakeCall) {
this.buffer = buffer;
this.interval = interval;
@@ -23,7 +26,7 @@ public class Consumer implements Runnable {
/**
* Run function for the Consumer
- * This Function checks randomly if the buffer has Cars and Pops them if that is the case.
+ * This Function checks randomly if the buffer has Workitems and Pops them if that is the case.
* If the buffer is full it wakens the sleeping consumers.
*
*/
diff --git a/ErzeugerVerbraucher/src/Producer.java b/ErzeugerVerbraucher/src/Producer.java
index 716b190..f508109 100644
--- a/ErzeugerVerbraucher/src/Producer.java
+++ b/ErzeugerVerbraucher/src/Producer.java
@@ -23,7 +23,7 @@ public class Producer implements Runnable {
/**
* Run Function for the Producer
- * This function Produces Cars randomly when the Buffer is not full.
+ * This function Produces Workitems randomly when the Buffer is not full.
* If the Buffer is empty it wakens the Sleeping Producers
*/
@Override
--
GitLab