feat(dissertation): add vdmj explanation

This commit is contained in:
Anthony Berg 2024-05-15 18:08:39 +01:00
parent 5724fb91f3
commit 5e03b65a0b
6 changed files with 146 additions and 9 deletions

View File

@ -260,6 +260,66 @@ Brief overview of what it is supposed to do... % TODO
\end{itemize}
\subsection{VDMJ Wrapper}
\begin{itemize}
\item VDMJ is written in Java and it is free open source software that is accessible on
GitHub
\item This allows for VDMJ to be used as per the license, GNU General Public License v3
(GPLv3)~\cite{vdmj:license}~\cite{gpl3}. This means that as VDMJ is being used as a
library, the code for this project has to be licensed with GPLv3 or any GPLv3 compatible
license~\cite{gpl3:library}
\end{itemize}
\subsubsection{Implementing VDMJ}
\begin{itemize}
\item VDMJ has packages available on Maven Central making adding it as a dependency simple
\item The package used was \lstinline|dk.au.ece.vdmj:vdmj| with version \lstinline|4.5.0|
\item However, initially when implementing VDMJ, \lstinline|4.5.0-P| was used accidentally
and it led to debugging why imports were not working; and therefore the \lstinline|-P|
versions are not suitable
\item The initial method of implementation was using a Ktor server that would have run
alongside the desktop application, where the server would handle Representational State Transfer (REST)
API calls
\item This was unnecessary as the \textit{interactive} mode of VDMJ was able to run on
the desktop application itself. However, the Ktor was useful for debugging and testing as
an API route was created to allow VDMJ commands to be executed through a URL
\item To be able to get the outputs from VDMJ, a \lstinline|ConsolePrintWriter| new had to be
created from the \lstinline|com.fujitsu.vdmj.messages| package; which handles writing to
the console \textit{stdout}. This then gets used to replace the \lstinline|Console.out| and
\lstinline|Console.err| in the \lstinline|com.fujitsu.vdmj.messages| package
\item Parsing commands into VDMJ interface - was more difficult
\footnote{The objects created here are provided by the \lstinline|java.io| package.}
\begin{itemize}
\item Created a \lstinline|PipedInputStream| object, that gets connected to a \lstinline|PipedOutputStream|
object by passing the latter object in as a parameter. The \lstinline|PipedOutputStream| is then used
to pass inputs into \lstinline|PipedInputStream|
\item To be able to write to this stream, a \lstinline|BufferedWriter| is created by passing the \lstinline|PipedOutputStream|
with a bridge \lstinline|OutputStreamWriter| that encodes characters into bytes
\item For VDMJ to be able to read the input stream, a separate object had to be created, \lstinline|BufferedReader|,
where the \lstinline|PipedInputStream| gets parsed through a bridge, \lstinline|InputStreamReader| that converts
bytes to characters
% TODO create a diagram of this (better than having code)
% BufferedWriter -> encode to byte -> Stream -> decode to char -> VDMJ
\end{itemize}
\end{itemize}
\begin{listing}
\inputminted[
linenos,
breaklines,
]{kotlin}{code/vdmj-interact.kt}
\caption[VDMJ IO Stream]{Snippet of controlling VDMJ interactive mode Input/Output streams}
\label{list:vdmj-io}
\end{listing}
\subsubsection{Handling VDMJ Outputs}
\begin{itemize}
\item VDMJ outputs are handled using string manipulation
\item Created into objects that are replicas of types in VDM-SL
\item The string manipulation allows to specify where the outputs
of the object go
\end{itemize}
% Talk about how XPC was used here, not how it was implemented

View File

@ -0,0 +1,55 @@
package io.anthonyberg.connector.shared.vdmj
import com.fujitsu.vdmj.messages.Console
import com.fujitsu.vdmj.messages.ConsolePrintWriter
import com.fujitsu.vdmj.plugins.VDMJ
import java.io.*
object VDMJ {
// Create a ByteArrayOutputStream to capture the output
private val byteArrayOutputStream = ByteArrayOutputStream()
private val printStream = ConsolePrintWriter(byteArrayOutputStream)
// Input handlers
private val inputStream = PipedInputStream()
private val inputOutput = PipedOutputStream(inputStream)
private val bufferedReader = BufferedReader(InputStreamReader(inputStream))
private val writer = BufferedWriter(OutputStreamWriter(inputOutput))
// Save the old PrintStreams
private val oldOut = Console.out
private val oldErr = Console.err
private val oldIn = Console.`in`
init {
//VDMJ Initialization
// Redirect Console's PrintStreams to the new PrintStream
Console.out = printStream
Console.err = printStream
Console.`in` = bufferedReader
// Rest of VDMJ setup
}
suspend fun run(command: String): String {
// Clean previous console outputs
byteArrayOutputStream.reset()
// Run commands
withContext(Dispatchers.IO) {
writer.write(command)
writer.write(System.lineSeparator())
writer.flush()
}
// Convert the captured output to a string
var output = byteArrayOutputStream.toString()
// Clear console output again
byteArrayOutputStream.reset()
return VDMJExpression(output = output)
}
}

Binary file not shown.

View File

@ -0,0 +1 @@
2634

View File

@ -59,8 +59,6 @@
\usepackage{graphicx}
\usepackage{verbatim}
% For word counts
\immediate\write18{texcount -1 -sum -inc \jobname.tex -out=\jobname.sum}

View File

@ -93,13 +93,6 @@
urldate = {2024-02-23},
}
@online{vdmj,
author = {Nick Battle},
title = {VDMJ},
url = {https://github.com/nickbattle/vdmj},
urldate = {2024-04-21},
}
@manual{overture-remote,
author = {Peter Gorm Larsen and Kenneth Lausdahl and Peter Jørgensen and Joey
Coleman and Sune Wolff and Nick Battle},
@ -274,6 +267,36 @@
urldate = {2024-05-14},
}
@online{vdmj,
author = {Nick Battle},
title = {VDMJ},
url = {https://github.com/nickbattle/vdmj},
urldate = {2024-04-21},
}
@online{vdmj:license,
author = {Nick Battle},
title = {vdmj/LICENCE at master · nickbattle/vdmj},
url = {https://github.com/nickbattle/vdmj/blob/master/LICENCE},
urldate = {2024-05-14},
}
@online{gpl3,
author = {{Free Software Foundation, Inc.}},
title = {The GNU General Public License v3.0 - GNU Project - Free Software
Foundation},
url = {https://www.gnu.org/licenses/gpl-3.0.en.html},
urldate = {2024-05-14},
}
@online{gpl3:library,
author = {{Free Software Foundation, Inc.}},
title = {Frequently Asked Questions about the GNU Licenses - GNU Project -
Free Software Foundation},
url = {https://www.gnu.org/licenses/gpl-faq.html#IfLibraryIsGPL},
urldate = {2024-05-14},
}
@online{xpc:pom,
author = {Mike Frizzell},
title = {Maven Folder Structure Re-org by frizman21 · Pull Request \#227 ·