Initial commit.

.gitattributes

@@ -0,0 +1,8 @@
+* text=auto !eol
+*.scala text eol=lf
+*.sc text eol=lf
+*.sh text eol=lf
+*.properties text eol=lf
+*.bat text eol=crlf
+*.cmd text eol=crlf
+*.ps1 text eol=crlf

.github/workflows/CI.yml

@@ -0,0 +1,17 @@
+name: CI
+
+on: [push]
+
+jobs:
+
+  build-ubuntu:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+        with:
+          submodules: recursive
+      - name: Verify
+        run: |
+          (DIR=kekinian && SIREUM_V=master && export SIREUM_NO_SETUP=true && rm -fR $DIR && mkdir -p $DIR/bin && cd $DIR/bin && curl -JLso init.sh https://raw.githubusercontent.com/sireum/kekinian/$SIREUM_V/bin/init.sh && bash init.sh)
+          SIREUM_HOME=`pwd`/kekinian bin/test.cmd 

.gitignore

@@ -0,0 +1,6 @@
+/.idea
+/.idea_modules
+/test
+out
+*.cmd.jar
+*.cmd.com

bin/project.cmd

@@ -0,0 +1,48 @@
+::/*#! 2> /dev/null                                 #
+@ 2>/dev/null # 2>nul & echo off & goto BOF         #
+if [ -z ${SIREUM_HOME} ]; then                      #
+  echo "Please set SIREUM_HOME env var"             #
+  exit -1                                           #
+fi                                                  #
+exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@"  #
+:BOF
+setlocal
+if not defined SIREUM_HOME (
+  echo Please set SIREUM_HOME env var
+  exit /B -1
+)
+%SIREUM_HOME%\bin\sireum.bat slang run "%0" %*
+exit /B %errorlevel%
+::!#*/
+// #Sireum
+
+import org.sireum._
+import org.sireum.project.{Module, Project, Target}
+
+val home = Os.slashDir.up.canon
+
+val srcMain = Os.path("src") / "main"
+
+val upgrader = Module(
+  id = "upgrader",
+  basePath = (home / "upgrader").string,
+  subPathOpt = None(),
+  deps = ISZ(),
+  targets = ISZ(Target.Jvm),
+  ivyDeps = ISZ(
+    "org.sireum.kekinian::library:",
+    "org.antlr:antlr4-runtime:"
+  ),
+  sources = ISZ(
+    (srcMain / "java").string,
+    (srcMain / "scala").string
+  ),
+  resources = ISZ(),
+  testSources = ISZ(),
+  testResources = ISZ(),
+  publishInfoOpt = None()
+)
+
+val prj = Project.empty + upgrader
+
+println(project.JSON.fromProject(prj, T))

bin/test.cmd

@@ -0,0 +1,54 @@
+::/*#! 2> /dev/null                                 #
+@ 2>/dev/null # 2>nul & echo off & goto BOF         #
+if [ -z ${SIREUM_HOME} ]; then                      #
+  echo "Please set SIREUM_HOME env var"             #
+  exit -1                                           #
+fi                                                  #
+exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@"  #
+:BOF
+setlocal
+if not defined SIREUM_HOME (
+  echo Please set SIREUM_HOME env var
+  exit /B -1
+)
+%SIREUM_HOME%\bin\sireum.bat slang run "%0" %*
+exit /B %errorlevel%
+::!#*/
+// #Sireum
+
+import org.sireum._
+
+val home = Os.slashDir.up.canon
+
+val test = home / "test"
+val testExamples = test / "v3-logika-examples"
+val testResult = test / "result"
+val ext: String = "logika"
+val assembly = home / "out" / "logika-upgrader" / "assemble" / "logika-upgrader.jar.bat"
+
+test.mkdirAll()
+testResult.removeAll()
+testResult.mkdirAll()
+
+println("Building logika-upgrader ...")
+assert(Sireum.run(ISZ("proyek", "assemble", "--jar", "logika-upgrader", "--uber", "--main", "Upgrader", home.string)) == 0)
+println()
+
+println(s"Preparing $testExamples ...")
+if (!testExamples.exists) {
+  proc"git clone https://github.com/sireum/v3-logika-examples".echo.console.at(test).runCheck()
+} else {
+  proc"git clean -xdf".echo.console.at(testExamples).runCheck()
+  proc"git pull".echo.console.at(testExamples).runCheck()
+}
+println()
+
+println(s"Upgrading examples ...")
+val env = ISZ[(String, String)]("PATH" ~> s"${Sireum.javaHomeOpt.get}${Os.pathSepChar}${Os.env("PATH")}")
+for (p <- Os.Path.walk(testExamples, F, F, (f: Os.Path) => f.ext == ext)) {
+  val rel = testExamples.relativize(p).string
+  val out = testResult / ops.StringOps(rel).substring(0, rel.size - ext.size - 1)
+  proc"$assembly $p $out".echo.console.env(env).runCheck()
+  println()
+}
+

license.txt

@@ -0,0 +1,22 @@
+Copyright (c) 2023, Robby, Kansas State University
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+1. Redistributions of source code must retain the above copyright notice, this
+   list of conditions and the following disclaimer.
+2. Redistributions in binary form must reproduce the above copyright notice,
+   this list of conditions and the following disclaimer in the documentation
+   and/or other materials provided with the distribution.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR
+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
+ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

readme.md

@@ -0,0 +1,56 @@
+# Logika v3 to Kekinian Upgrader
+
+This repository holds [Logika v3](https://logika.v3.sireum.org) truth table and propositional/predicate/programming 
+logic proof to the new [Logika version](https://sireum.org).
+
+The upgrader uses a syntax-based translation, thus, further tweaking may be required on some examples
+(e.g., truth tables involving the implication operator due to column sensitivity and operator number of characters, 
+programming logic involving sequence updates due to differences in generated claims, conditional proof function
+definitions, or range quantification due to the new use of short-circuit implication/conjunction).
+
+Note that Sireum IVE/IntelliJ's "Edit -> Column Selection Mode" is handy when adjusting a multiline character column in
+truth tables.
+
+## Requirement
+
+* [Sireum](https://sireum.org/getting-started/)
+
+## How To Use
+
+1. Clone this repo locally and build the upgrader jar/batch file:
+
+   ```
+   git clone https://github.com/sireum/logika-upgrader
+   sireum proyek assemble --jar logika-upgrader --uber --main Upgrader logika-upgrader
+   ```
+
+2. Run the batch file:
+
+   * On **macOS/Linux**:
+
+     ```sh
+     out/logika-upgrader/assemble/logika-upgrader.jar.bat
+     ```
+
+   * On **Windows**:
+
+     ```cmd
+     out\logika-upgrader\assemble\logika-upgrader.jar.bat
+     ```
+
+   which will display its usage information:
+
+   ```
+   Usage: <input> [ <output> ] [ auto ] 
+   ```
+   
+   The verifier assumes verified Logika v3 file as its `<input>`.
+   If the `<output>` file is specified, then the '.logika'/'.sc' file extension for truth table/other.
+   The last `auto` option should used for programming logic Auto or SymExe Logika v3 mode (by default
+   the upgrader detects auto mode by determining whether `auto` or `symexe` is in the (lower-cased) `<input>` path. 
+
+## Test
+
+Execute [bin/test.cmd](bin/test.cmd) to run the upgrader on https://github.com/sireum/v3-logika-examples to see
+example results (and tweaking needed compared to the corresponding hand-translated examples at 
+https://github.com/sireum/logika-examples).