Parse modelgen options.

Makefile

@@ -56,13 +56,24 @@ DROP_ROOT=$(subst $(GIT_ROOT)/,./,$1)
 
 # You have to perform the mvn build first to have the project deps installed.
 mvn: $(BUILD_MVN_BIN)/evbt
+	@rm -f evbt
+	@ln -s $(BUILD_MVN_BIN)/evbt
+	@echo Use ./evbt
+
 # Now you can perform a javac compile with a slightly quicker rebuild time.
 # It cannot rebuild the generated classes from antlr, so if you change the grammar
 # then you have to rerun "make mvn"
 javac: $(BUILD_JAVAC_BIN)/evbt
+	@rm -f evbt
+	@ln -s $(BUILD_JAVAC_BIN)/evbt
+	@echo Use ./evbt
+
 # Or a native compile, with a much much longer rebuild time.
 # Do this when you have a build that passes the test suite.
 graal: $(BUILD_GRAAL_BIN)/evbt
+	@rm -f evbt
+	@ln -s $(BUILD_GRAAL_BIN)/evbt
+	@echo Use ./evbt
 
 # Make sure the output directories exist.
 $(shell mkdir -p $(BUILD) $(PROJECT_DEPS) $(GEN_ANTLR4))

src/main/java/com/viklauverk/eventbtools/CommandLine.java

@@ -1,6 +1,6 @@
 /*
  Copyright (C) 2021 Viklauverk AB
- 
+
  This program is free software: you can redistribute it and/or modify
  it under the terms of the GNU Affero General Public License as published by
  the Free Software Foundation, either version 3 of the License, or
@@ -21,8 +21,8 @@
 import com.viklauverk.eventbtools.core.LogLevel;
 import com.viklauverk.eventbtools.core.LogModule;
 import com.viklauverk.eventbtools.core.ShowSettings;
-import com.viklauverk.eventbtools.core.CodeGenSettings;
-import com.viklauverk.eventbtools.core.DocGenSettings;
+import com.viklauverk.eventbtools.core.ModelGenSettings;
+import com.viklauverk.eventbtools.core.ModelTarget;
 import com.viklauverk.eventbtools.core.RenderTarget;
 import com.viklauverk.eventbtools.core.Settings;
 import com.viklauverk.eventbtools.core.Util;
@@ -59,6 +59,7 @@ public static Cmd parse(Settings s, String[] args)
         case CONSOLE:  args = parseConsole(s, args); break;
         case DOCGEN: args = parseDocGen(s, args); break;
         case DOCMOD: args = parseDocMod(s, args); break;
+        case MODELGEN: args = parseModelGen(s, args); break;
         case EDK: args = parseEDK(s, args); break;
         case SHOW:  args = parseShow(s, args); break;
         case HELP: args = parseHelp(s, args); break;
@@ -320,6 +321,47 @@ else if (args.length != 0)
         return args;
     }
 
+    private static String[] parseModelGen(Settings s, String[] args)
+    {
+        for (;;)
+        {
+            args = handleGlobalOption(s, args);
+            if (args.length == 0) break;
+
+            String arg = args[0];
+
+            if (!arg.startsWith("--")) break;
+
+            LogModule.usageErrorStatic("Unknown option \"%s\"", arg);
+        }
+
+        if (args.length < 2)
+        {
+            log.usageError("Usage: evbt modelgen [options] <why3> <dir>");
+            System.exit(1);
+        }
+
+        ModelTarget mt = ModelTarget.lookup(args[0]);
+        if (mt == null)
+        {
+            log.usageError("Not a supported model target \""+args[0]+"\", available targets are: why3");
+        }
+
+        s.modelGenSettings().setModelTarget(mt);
+        args = Util.shiftLeft(args);
+
+        s.commonSettings().setSourceDir(args[0]);
+        args = Util.shiftLeft(args);
+
+        while(args.length > 0)
+        {
+            s.commonSettings().addMachineOrContext(args[0]);
+            args = Util.shiftLeft(args);
+        }
+
+        return args;
+    }
+
     private static String[] parseEDK(Settings s, String[] args)
     {
         for (;;)

src/main/java/com/viklauverk/eventbtools/core/LogModuleNames.java

@@ -1,4 +1,4 @@
-// Copyright Viklauverk AB 2021
+// Copyright Viklauverk AB 2021-2023
 // Generated by "make logmodules"
 package com.viklauverk.eventbtools.core;
 public enum LogModuleNames
@@ -16,10 +16,11 @@ public enum LogModuleNames
 event,
 formula,
 htmq,
-implementation,
+implementationcpp,
 machine,
 main,
 match,
+modelgen,
 parser,
 pattern,
 planimplementation,
@@ -33,4 +34,5 @@ public enum LogModuleNames
 unicode,
 util,
 walkformula,
+why3,
 }

src/main/java/com/viklauverk/eventbtools/core/ModelGenSettings.java

@@ -1,5 +1,5 @@
 /*
- Copyright (C) 2021-2023 Viklauverk AB
+ Copyright (C) 2021-2024 Viklauverk AB
 
  This program is free software: you can redistribute it and/or modify
  it under the terms of the GNU Affero General Public License as published by
@@ -39,9 +39,9 @@ public ModelTarget modelTarget()
         return model_target_;
     }
 
-    public void setModelTarget(ModelTarget rt)
+    public void setModelTarget(ModelTarget mt)
     {
-        model_target_ = rt;
+        model_target_ = mt;
     }
 
 }

src/main/java/com/viklauverk/eventbtools/core/ModelGenWhy3.java

@@ -1,5 +1,5 @@
 /*
- Copyright (C) 2021-2023 Viklauverk AB
+ Copyright (C) 2024 Viklauverk AB
 
  This program is free software: you can redistribute it and/or modify
  it under the terms of the GNU Affero General Public License as published by
@@ -54,12 +54,12 @@ public String generateModel() throws Exception
 
         for (String ctx : sys().contextNames())
         {
-            cnvs.append("EVBT(eb.show.part \""+ctx+"\")\n");
+            cnvs.append("EVBT(mo.show.part \""+ctx+"\")\n");
         }
 
         for (String mch : sys().machineNames())
         {
-            cnvs.append("EVBT(eb.show.part \""+mch+"\")\n");
+            cnvs.append("EVBT(mo.show.part \""+mch+"\")\n");
         }
         return cnvs.render();
     }