de.uka.ilkd.key.smt

Class Pipe<T>

java.lang.Object

de.uka.ilkd.key.smt.Pipe<T>

class Pipe<T>
extends java.lang.Object

On each side of the pipe there are sender and receivers: Receiver ====<=Output======= Sender ****************** KeY* Sender ======Input=>====== Receiver *External Process* Receiver ====<=Error======== Sender ******************

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private class	Pipe.Receiver Waits until a message is received from the other side of the pipe.
private class	Pipe.Sender Mainly consists of a queue for messages.
private class	Pipe.Worker Worker class for both the receiver and sender of the pipe.

Field Summary

Fields

Modifier and Type	Field and Description
static int	ERROR_MESSAGE
private java.util.concurrent.locks.ReentrantLock	listenerLock
private java.util.LinkedList<PipeListener<T>>	listeners
private java.lang.String[]	messageDelimiters The delimiters of the messages, i.e. strings that indicate the end of a message.
static int	NORMAL_MESSAGE
private java.util.concurrent.locks.Condition	postMessages The sender goes to sleep when there are no messages to be sent.
private java.util.LinkedList<java.lang.String>	queue Stores messages that are to be sent in the next cycle of the worker responsible for sending messages.
private java.util.concurrent.locks.ReentrantLock	queueLock
private T	session User specific data.
private java.util.concurrent.locks.ReentrantLock	workerLock
private java.util.List<Pipe.Worker>	workers The workers of the pipe.

Constructor Summary

Constructors

Constructor and Description
Pipe(T session, java.lang.String[] messageDelimiters)

Method Summary

Modifier and Type	Method and Description
(package private) void	addListener(PipeListener<T> listener)
void	close()
(package private) void	closeSendingPipe() Closes the pipe for sending, signalling the end of the input to the target process.
T	getSession()
(package private) void	sendMessage(java.lang.String message) sends a message to the external process.
void	start(java.io.InputStream input, java.io.OutputStream output, java.io.InputStream error, PipeListener<T> listener)
void	waitForPipe() Wait until the output of the target process has been read completely.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

listenerLock

private final java.util.concurrent.locks.ReentrantLock listenerLock

listeners

private final java.util.LinkedList<PipeListener<T>> listeners

workers

private java.util.List<Pipe.Worker> workers

The workers of the pipe. One worker is responsible for sending messages, while the other two workers handle messages which are received.

workerLock

private final java.util.concurrent.locks.ReentrantLock workerLock

queue

private java.util.LinkedList<java.lang.String> queue

Stores messages that are to be sent in the next cycle of the worker responsible for sending messages.

queueLock

private final java.util.concurrent.locks.ReentrantLock queueLock

postMessages

private final java.util.concurrent.locks.Condition postMessages

The sender goes to sleep when there are no messages to be sent. If you want to wake him up, use this condition.

messageDelimiters

private final java.lang.String[] messageDelimiters

The delimiters of the messages, i.e. strings that indicate the end of a message. If you specify several delimiters a single message is chosen as small as possible, i.e., it does not contain any delimiter.

NORMAL_MESSAGE

public static final int NORMAL_MESSAGE

See Also:

Constant Field Values

ERROR_MESSAGE

public static final int ERROR_MESSAGE

See Also:

Constant Field Values

session

private final T session

User specific data.

Constructor Detail

Pipe

public Pipe(T session,
            java.lang.String[] messageDelimiters)

Method Detail

start

public void start(java.io.InputStream input,
                  java.io.OutputStream output,
                  java.io.InputStream error,
                  PipeListener<T> listener)

close

public void close()

sendMessage

void sendMessage(java.lang.String message)

sends a message to the external process. Mainly it adds a new message to the message queue and wakes up the sender.

closeSendingPipe

void closeSendingPipe()

Closes the pipe for sending, signalling the end of the input to the target process.

addListener

void addListener(PipeListener<T> listener)

getSession

public T getSession()

waitForPipe

public void waitForPipe()
                 throws java.lang.InterruptedException

Wait until the output of the target process has been read completely.

Throws:

java.lang.InterruptedException