diff --git a/pub/dissertation/chapters/design.tex b/pub/dissertation/chapters/design.tex index dec16f6..0a9e572 100644 --- a/pub/dissertation/chapters/design.tex +++ b/pub/dissertation/chapters/design.tex @@ -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 diff --git a/pub/dissertation/code/vdmj-interact.kt b/pub/dissertation/code/vdmj-interact.kt new file mode 100644 index 0000000..1102e71 --- /dev/null +++ b/pub/dissertation/code/vdmj-interact.kt @@ -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) + } +} diff --git a/pub/dissertation/dissertation.pdf b/pub/dissertation/dissertation.pdf index 4f919a9..663511c 100644 Binary files a/pub/dissertation/dissertation.pdf and b/pub/dissertation/dissertation.pdf differ diff --git a/pub/dissertation/dissertation.sum b/pub/dissertation/dissertation.sum new file mode 100644 index 0000000..1c4c2de --- /dev/null +++ b/pub/dissertation/dissertation.sum @@ -0,0 +1 @@ +2634 diff --git a/pub/dissertation/dissertation.tex b/pub/dissertation/dissertation.tex index c6f64b7..09870d7 100644 --- a/pub/dissertation/dissertation.tex +++ b/pub/dissertation/dissertation.tex @@ -59,8 +59,6 @@ \usepackage{graphicx} -\usepackage{verbatim} - % For word counts \immediate\write18{texcount -1 -sum -inc \jobname.tex -out=\jobname.sum} diff --git a/pub/dissertation/references.bib b/pub/dissertation/references.bib index bb311fb..582813d 100644 --- a/pub/dissertation/references.bib +++ b/pub/dissertation/references.bib @@ -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 ·