diff --git a/Makefile b/Makefile
index c127154..9360590 100644
--- a/Makefile
+++ b/Makefile
@@ -1,4 +1,4 @@
-# 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
diff --git a/src/main/java/com/viklauverk/eventbtools/core/AllRenders.java b/src/main/java/com/viklauverk/eventbtools/core/AllRenders.java
index 41b03ee..f89ca41 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/AllRenders.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/AllRenders.java
@@ -121,11 +121,6 @@ public void walkTheory(Theory t, String pattern)
VisitTheory.walk(rt_, t, pattern);
}
- public void walkPolymorphicDataType(PolymorphicDataType pdt, String pattern)
- {
- VisitPolymorphicDataType.walk(rpdt_, pdt, pattern);
- }
-
public void walkContext(Context c, String pattern)
{
VisitContext.walk(rc_, c, pattern);
@@ -141,6 +136,11 @@ public void walkEvent(Event e, String pattern)
VisitEvent.walk(re_, e, pattern);
}
+ public void walkPolymorphicDataType(PolymorphicDataType pdt, String pattern)
+ {
+ VisitPolymorphicDataType.walk(rpdt_, pdt, pattern);
+ }
+
public void walkFormula(Formula i)
{
VisitFormula.walk(rf_, i);
diff --git a/src/main/java/com/viklauverk/eventbtools/core/ConsoleExecutor.java b/src/main/java/com/viklauverk/eventbtools/core/ConsoleExecutor.java
index fe5431f..57695ab 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/ConsoleExecutor.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/ConsoleExecutor.java
@@ -62,7 +62,17 @@ String go()
String args = line_.substring(index_);
CmdCommon cco = cmd.constructor.create(console_, args);
log.debug("Executing cmd %s on line >%s<\n", cmd, args);
- return cco.go();
+ String response = "";
+ try
+ {
+ response = cco.go();
+ }
+ catch (Exception e)
+ {
+ e.printStackTrace(System.err);
+ response = "CAUGHT: "+e.toString();
+ }
+ return response;
}
void skipWhitespace()
diff --git a/src/main/java/com/viklauverk/eventbtools/core/DocGenTeX.java b/src/main/java/com/viklauverk/eventbtools/core/DocGenTeX.java
index d8c2c9b..c176587 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/DocGenTeX.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/DocGenTeX.java
@@ -97,7 +97,7 @@ public String generateDocument() throws Exception
cnvs.append("\\pagebreak\n\n");
cnvs.append("\\section{\\KEYWL{CONTEXT}\\small\\ "+Util.texSafe(ctx)+" "+pos+"}\n\n");
- cnvs.append("EVBT(eb.show.part --tex "+ctx+")\n");
+ cnvs.append("EVBT(eb.show.part --tex ctx/"+ctx+")\n");
}
for (String mch : sys().machineNames())
@@ -115,7 +115,7 @@ public String generateDocument() throws Exception
}
cnvs.append("\\section{\\KEYWL{"+m.machineOrRefinement().toUpperCase()+"}\\small\\ "+Util.texSafe(mch)+" "+pos+"}\n\n");
- cnvs.append("EVBT(eb.show.part --tex "+mch+")\n");
+ cnvs.append("EVBT(eb.show.part --tex mch/"+mch+")\n");
}
for (String thr : sys().deployedTheoryNames())
@@ -133,7 +133,7 @@ public String generateDocument() throws Exception
}
cnvs.append("\\section{\\KEYWL{THEORY}\\small\\ "+Util.texSafe(thr)+" "+pos+"}\n\n");
- cnvs.append("EVBT(eb.show.part --tex "+thr+")\n");
+ cnvs.append("EVBT(eb.show.part --tex thr/"+thr+")\n");
}
cnvs.append("\\printindex\n");
diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderContext.java b/src/main/java/com/viklauverk/eventbtools/core/RenderContext.java
index c301919..02e1c16 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/RenderContext.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/RenderContext.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
@@ -48,29 +48,24 @@ public void visit_AxiomsEnd(Context ctx) { }
public void visit_ContextEnd(Context ctx) { }
- protected String buildContextPartName(Context ctx)
- {
- return ctx.name();
- }
-
- protected String buildContextSetsPartName(Context ctx)
+ public static String buildContextPartName(Context ctx)
{
- return ctx.name()+"/sets";
+ return "ctx/"+ctx.name();
}
- protected String buildContextSetPartName(Context ctx, CarrierSet set)
+ public static String buildSetPartName(Context ctx, CarrierSet set)
{
- return ctx.name()+"/constant/"+set.name();
+ return "ctx/"+ctx.name()+"/set/"+(set!=null?set.name():"");
}
- protected String buildContextConstantsPartName(Context ctx)
+ public static String buildConstantPartName(Context ctx, Constant con)
{
- return ctx.name()+"/constants";
+ return "ctx/"+ctx.name()+"/constant/"+(con!=null?con.name():"");
}
- protected String buildContextConstantPartName(Context ctx, Constant con)
+ public static String buildAxiomPartName(Context ctx, Axiom axm)
{
- return ctx.name()+"/constant/"+con.name();
+ return "ctx/"+ctx.name()+"/axiom/"+(axm!=null?axm.name():"");
}
diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderContextSearch.java b/src/main/java/com/viklauverk/eventbtools/core/RenderContextSearch.java
index 2628cfe..e71d0b6 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/RenderContextSearch.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/RenderContextSearch.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
@@ -19,4 +19,27 @@
public class RenderContextSearch extends RenderContext
{
+ @Override
+ public void visit_ContextStart(Context ctx)
+ {
+ renders().search().addPart(buildContextPartName(ctx));
+ }
+
+ @Override
+ public void visit_Set(Context ctx, CarrierSet set)
+ {
+ renders().search().addPart(buildSetPartName(ctx, set));
+ }
+
+ @Override
+ public void visit_Constant(Context ctx, Constant cnst)
+ {
+ renders().search().addPart(buildConstantPartName(ctx, cnst));
+ }
+
+ @Override
+ public void visit_Axiom(Context ctx, Axiom axm)
+ {
+ renders().search().addPart(buildAxiomPartName(ctx, axm));
+ }
}
diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderEvent.java b/src/main/java/com/viklauverk/eventbtools/core/RenderEvent.java
index bf71742..0eb5dc6 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/RenderEvent.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/RenderEvent.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
@@ -54,39 +54,29 @@ public void visit_ActionsEnd(Event eve) { }
public void visit_EventEnd(Event eve) { }
- protected String buildEventPartName(Event e)
- {
- return e.machine().name()+"/"+e.name();
- }
-
- protected String buildParametersPartName(Event e)
- {
- return e.machine().name()+"/"+e.name()+"/parameters";
- }
-
- protected String buildParameterPartName(Event e, Variable var)
+ protected static String buildEventPartName(Event e)
{
- return e.machine().name()+"/"+e.name()+"/parameter/"+var.name();
+ return "mch/"+e.machine().name()+"/event/"+e.name();
}
- protected String buildGuardsPartName(Event e)
+ protected static String buildParameterPartName(Event e, Variable var)
{
- return e.machine().name()+"/"+e.name()+"/guards";
+ return "mch/"+e.machine().name()+"/event/"+e.name()+"/parameter/"+var.name();
}
- protected String buildGuardPartName(Event e, Guard g)
+ protected static String buildGuardPartName(Event e, Guard g)
{
- return e.machine().name()+"/"+e.name()+"/guard/"+g.name();
+ return "mch/"+e.machine().name()+"/event/"+e.name()+"/guard/"+g.name();
}
- protected String buildActionsPartName(Event e)
+ protected static String buildWitnessPartName(Event e, Witness wtn)
{
- return e.machine().name()+"/"+e.name()+"/actions";
+ return "mch/"+e.machine().name()+"/event/"+e.name()+"/witness/"+wtn.name();
}
- protected String buildActionPartName(Event e, Action a)
+ protected static String buildActionPartName(Event e, Action a)
{
- return e.machine().name()+"/"+e.name()+"/action/"+a.name();
+ return "mch/"+e.machine().name()+"/event/"+e.name()+"/action/"+a.name();
}
}
diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderEventSearch.java b/src/main/java/com/viklauverk/eventbtools/core/RenderEventSearch.java
index 5fe9eeb..4e8d052 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/RenderEventSearch.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/RenderEventSearch.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
@@ -19,4 +19,35 @@
public class RenderEventSearch extends RenderEvent
{
+ @Override
+ public void visit_EventStart(Event eve)
+ {
+ renders().search().addPart(buildEventPartName(eve));
+ }
+
+ @Override
+ public void visit_Parameter(Event eve, Variable prm)
+ {
+ renders().search().addPart(buildParameterPartName(eve, prm));
+ }
+
+ @Override
+ public void visit_Guard(Event eve, Guard grd)
+ {
+ renders().search().addPart(buildGuardPartName(eve, grd));
+ }
+
+ @Override
+ public void visit_Witness(Event eve, Witness wtn)
+ {
+ renders().search().addPart(buildWitnessPartName(eve, wtn));
+ }
+
+ @Override
+ public void visit_Action(Event eve, Action act)
+ {
+ renders().search().addPart(buildActionPartName(eve, act));
+ }
+
+
}
diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderEventUnicode.java b/src/main/java/com/viklauverk/eventbtools/core/RenderEventUnicode.java
index 14a72d7..3c53c98 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/RenderEventUnicode.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/RenderEventUnicode.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
@@ -95,8 +95,6 @@ public void visit_HeadingComplete(Event eve)
@Override
public void visit_ParametersStart(Event eve)
{
- String id = buildParametersPartName(eve);
-
cnvs().startLine();
cnvs().keyword("any");
cnvs().endLine();
diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderMachine.java b/src/main/java/com/viklauverk/eventbtools/core/RenderMachine.java
index fde9e3f..1e9b922 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/RenderMachine.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/RenderMachine.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
@@ -54,35 +54,24 @@ public void visit_EventsEnd(Machine mch) { }
public void visit_MachineEnd(Machine mch) { }
- protected String buildMachinePartName(Machine mch)
- {
- return mch.name();
- }
-
- protected String buildMachineVariablesPartName(Machine mch)
+ protected static String buildMachinePartName(Machine mch)
{
- return mch.name()+"/variables";
+ return "mch/"+(mch!=null?mch.name():"");
}
- protected String buildMachineVariablePartName(Machine mch, Variable var)
+ protected static String buildMachineVariablePartName(Machine mch, Variable var)
{
- return mch.name()+"/variable/"+var.name();
+ return "mch/"+mch.name()+"/variable/"+(var!=null?var.name():"");
}
- protected String buildMachineInvariantsPartName(Machine mch)
+ protected static String buildMachineInvariantPartName(Machine mch, Invariant inv)
{
- return mch.name()+"/invariants";
+ return "mch/"+mch.name()+"/invariant/"+(inv!=null?inv.name():"");
}
- protected String buildMachineInvariantPartName(Machine mch, Invariant inv)
+ protected static String buildMachineVariantPartName(Machine mch, Variant var)
{
- return mch.name()+"/invariant/"+inv.name();
+ return "mch/"+mch.name()+"/variant/"+(var!=null?var.name():"");
}
- protected String buildMachineEventsPartName(Machine mch)
- {
- return mch.name()+"/events";
- }
-
-
}
diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderMachineSearch.java b/src/main/java/com/viklauverk/eventbtools/core/RenderMachineSearch.java
index 8930192..48f3e0b 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/RenderMachineSearch.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/RenderMachineSearch.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
@@ -30,25 +30,12 @@ public void visit_MachineStart(Machine mch)
renders().search().addPart(buildMachinePartName(mch));
}
- @Override
- public void visit_VariablesStart(Machine mch)
- {
- renders().search().addPart(buildMachineVariablesPartName(mch));
- }
-
@Override
public void visit_Variable(Machine mch, Variable variable)
{
renders().search().addPart(buildMachineVariablePartName(mch, variable));
}
-
- @Override
- public void visit_InvariantsStart(Machine mch)
- {
- renders().search().addPart(buildMachineInvariantsPartName(mch));
- }
-
@Override
public void visit_Invariant(Machine mch, Invariant invariant)
{
@@ -56,9 +43,9 @@ public void visit_Invariant(Machine mch, Invariant invariant)
}
@Override
- public void visit_EventsStart(Machine mch)
+ public void visit_Variant(Machine mch, Variant variant)
{
- renders().search().addPart(buildMachineEventsPartName(mch));
+ renders().search().addPart(buildMachineVariantPartName(mch, variant));
}
@Override
diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderOperator.java b/src/main/java/com/viklauverk/eventbtools/core/RenderOperator.java
deleted file mode 100644
index 3c7a2e0..0000000
--- a/src/main/java/com/viklauverk/eventbtools/core/RenderOperator.java
+++ /dev/null
@@ -1,37 +0,0 @@
-/*
- 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
- the Free Software Foundation, either version 3 of the License, or
- (at your option) any later version.
-
- This program is distributed in the hope that it will be useful,
- but WITHOUT ANY WARRANTY; without even the implied warranty of
- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- GNU Affero General Public License for more details.
-
- You should have received a copy of the GNU Affero General Public License
- along with this program. If not, see .
-*/
-
-package com.viklauverk.eventbtools.core;
-
-import java.util.List;
-import java.util.LinkedList;
-
-import com.viklauverk.eventbtools.core.Formula;
-
-public class RenderOperator extends CommonRenderFunctions
-{
- public void visit_OperatorStart(Operator oprt) { }
-
- public void visit_HeadingComplete(Operator oprt) { }
-
- public void visit_OperatorEnd(Operator oprt) { }
-
- protected String buildOperatorPartName(Operator oprt)
- {
- return oprt.theory().name()+"/"+oprt.name();
- }
-}
diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderOperatorUnicode.java b/src/main/java/com/viklauverk/eventbtools/core/RenderOperatorUnicode.java
deleted file mode 100644
index 569b0da..0000000
--- a/src/main/java/com/viklauverk/eventbtools/core/RenderOperatorUnicode.java
+++ /dev/null
@@ -1,60 +0,0 @@
-/*
- 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
- the Free Software Foundation, either version 3 of the License, or
- (at your option) any later version.
-
- This program is distributed in the hope that it will be useful,
- but WITHOUT ANY WARRANTY; without even the implied warranty of
- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- GNU Affero General Public License for more details.
-
- You should have received a copy of the GNU Affero General Public License
- along with this program. If not, see .
-*/
-
-package com.viklauverk.eventbtools.core;
-
-public class RenderOperatorUnicode extends RenderOperator
-{
- @Override
- public void visit_OperatorStart(Operator oprt)
- {
- String id = buildOperatorPartName(oprt);
-
- cnvs().marker(id);
-
- cnvs().startLine();
- if (oprt.notation() == OperatorNotationType.PREFIX)
- {
- cnvs().keywordLeft("prefix ");
- }
- if (oprt.notation() == OperatorNotationType.INFIX)
- {
- cnvs().keywordLeft("infix ");
- }
- cnvs().keywordLeft("operator ");
- cnvs().id(oprt.name());
- cnvs().endLine();
-
- if (oprt.hasComment())
- {
- cnvs().acomment(oprt.comment());
- }
- }
-
- @Override
- public void visit_HeadingComplete(Operator oprt)
- {
- }
-
- @Override
- public void visit_OperatorEnd(Operator oprt)
- {
- cnvs().startLine();
- cnvs().keyword("end");
- cnvs().endLine();
- }
-}
diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderPolymorphicDataType.java b/src/main/java/com/viklauverk/eventbtools/core/RenderPolymorphicDataType.java
index 94cf719..59e01ce 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/RenderPolymorphicDataType.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/RenderPolymorphicDataType.java
@@ -34,18 +34,13 @@ public void visit_ConstructorsEnd(PolymorphicDataType pdt) { }
public void visit_PolymorphicDataTypeEnd(PolymorphicDataType pdt) { }
- protected String buildPolymorphicDataTypePartName(PolymorphicDataType pdt)
+ protected static String buildPolymorphicDataTypePartName(PolymorphicDataType pdt)
{
- return pdt.theory().name()+"/"+pdt.baseName();
+ return "thr/"+pdt.theory().name()+"/datatype/"+pdt.baseName();
}
- protected String buildConstructorsPartName(PolymorphicDataType pdt)
+ protected static String buildConstructorPartName(PolymorphicDataType pdt, Constructor cnstr)
{
- return pdt.theory().name()+"/"+pdt.baseName()+"/constructors";
- }
-
- protected String buildConstructorPartName(PolymorphicDataType pdt, Constructor cnstr)
- {
- return pdt.theory().name()+"/"+pdt.baseName()+"/constructor/"+cnstr.name();
+ return "thr/"+pdt.theory().name()+"/datatype/"+pdt.baseName()+"/constructor/"+(cnstr!=null?cnstr.name():"");
}
}
diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderPolymorphicDataTypeTeX.java b/src/main/java/com/viklauverk/eventbtools/core/RenderPolymorphicDataTypeTeX.java
index c37752d..f483355 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/RenderPolymorphicDataTypeTeX.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/RenderPolymorphicDataTypeTeX.java
@@ -26,7 +26,6 @@ public void visit_PolymorphicDataTypeStart(PolymorphicDataType pdt)
cnvs().set(pdt.longName());
cnvs().append(" ");
cnvs().append("}\n");
- super.visit_PolymorphicDataTypeStart(pdt);
}
}
diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderPolymorphicDataTypeUnicode.java b/src/main/java/com/viklauverk/eventbtools/core/RenderPolymorphicDataTypeUnicode.java
index 5dc43e7..65a586f 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/RenderPolymorphicDataTypeUnicode.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/RenderPolymorphicDataTypeUnicode.java
@@ -32,27 +32,34 @@ public void visit_PolymorphicDataTypeStart(PolymorphicDataType pdt)
}
cnvs().startLine();
cnvs().id(pdt.longName());
+ if (pdt.hasConstructors())
+ {
+ cnvs().keyword(" ≜");
+ }
cnvs().endLine();
}
@Override
public void visit_ConstructorsStart(PolymorphicDataType pdt)
{
- cnvs().startLine();
- cnvs().keywordLeft("► ");
- cnvs().space();
}
@Override
public void visit_Constructor(PolymorphicDataType pdt, Constructor cnstr)
{
- //renders().walkConstructor(pdt, "");
+ cnvs().startAlignedLine();
+ cnvs().keywordLeft(" ► ");
+ cnvs().startMath();
+ cnvs().constructor(cnstr.name());
+ cnvs().stopMath();
+ cnvs().align();
+ cnvs().comment(cnstr.comment());
+ cnvs().stopAlignedLine();
}
@Override
public void visit_ConstructorsEnd(PolymorphicDataType pdt)
{
- cnvs().endLine();
}
@Override
@@ -63,8 +70,5 @@ public void visit_HeadingComplete(PolymorphicDataType pdt)
@Override
public void visit_PolymorphicDataTypeEnd(PolymorphicDataType pdt)
{
- cnvs().startLine();
- cnvs().keyword("end");
- cnvs().endLine();
}
}
diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderTheory.java b/src/main/java/com/viklauverk/eventbtools/core/RenderTheory.java
index 20b32f2..fa1284f 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/RenderTheory.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/RenderTheory.java
@@ -48,19 +48,24 @@ public void visit_AxiomsEnd(Theory thr) { }
public void visit_TheoryEnd(Theory thr) { }
- protected String buildTheoryPartName(Theory thr)
+ protected static String buildTheoryPartName(Theory thr)
{
- return thr.name();
+ return "thr/"+thr.name();
}
- protected String buildTheoryDataTypePartName(Theory thr, PolymorphicDataType pdt)
+ protected static String buildDataTypePartName(Theory thr, PolymorphicDataType pdt)
{
- return thr.name()+"/datatype/"+pdt.longName();
+ return "thr/"+thr.name()+"/datatype/"+(pdt!=null?pdt.longName():"");
}
- protected String buildOperatorPartName(Operator oprt)
+ protected static String buildOperatorPartName(Theory thr, Operator oprt)
{
- return oprt.name();
+ return "thr/"+thr.name()+"/operator/"+(oprt!=null?oprt.name():"");
+ }
+
+ protected static String buildAxiomPartName(Theory thr, Axiom axm)
+ {
+ return "thr/"+thr.name()+"/axiom/"+(axm!=null?axm.name():"");
}
}
diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderTheorySearch.java b/src/main/java/com/viklauverk/eventbtools/core/RenderTheorySearch.java
index cf9c95a..fe86555 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/RenderTheorySearch.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/RenderTheorySearch.java
@@ -26,12 +26,18 @@ public void visit_TheoryStart(Theory thr)
public void visit_Import(Theory thr, Theory ext) { }
+ public void visit_PolymorphicDataType(Theory thr, PolymorphicDataType pdt)
+ {
+ renders().walkPolymorphicDataType(pdt, "");
+ }
+
public void visit_Operator(Theory thr, Operator oprt)
{
- renders().search().addPart(buildOperatorPartName(oprt));
+ renders().search().addPart(RenderTheory.buildOperatorPartName(thr, oprt));
}
public void visit_Axiom(Theory thr, Axiom axiom)
{
+ renders().search().addPart(RenderTheory.buildAxiomPartName(thr, axiom));
}
}
diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderTheoryUnicode.java b/src/main/java/com/viklauverk/eventbtools/core/RenderTheoryUnicode.java
index ead8104..067c8cd 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/RenderTheoryUnicode.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/RenderTheoryUnicode.java
@@ -100,6 +100,30 @@ public void renderProofSummary(Theory thr)
cnvs().align();
cnvs().comment(oprt.comment());
cnvs().stopAlignedLine();
+
+/*
+ String id = buildOperatorPartName(oprt);
+
+ cnvs().marker(id);
+
+ cnvs().startLine();
+ if (oprt.notation() == OperatorNotationType.PREFIX)
+ {
+ cnvs().keywordLeft("prefix ");
+ }
+ if (oprt.notation() == OperatorNotationType.INFIX)
+ {
+ cnvs().keywordLeft("infix ");
+ }
+ cnvs().keywordLeft("operator ");
+ cnvs().id(oprt.name());
+ cnvs().endLine();
+
+ if (oprt.hasComment())
+ {
+ cnvs().acomment(oprt.comment());
+ }
+*/
}
@Override public void visit_OperatorsEnd(Theory thr)
diff --git a/src/main/java/com/viklauverk/eventbtools/core/SysCompleter.java b/src/main/java/com/viklauverk/eventbtools/core/SysCompleter.java
index bf8c377..14140ad 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/SysCompleter.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/SysCompleter.java
@@ -32,18 +32,13 @@ public void complete(LineReader reader,
{
int space= line.line().indexOf(" ");
if (space == -1) return;
-
String path = line.line().substring(space+1).trim();
- String[] parts = path.split("/");
+ List parts = sys_.listParts("");
- if (sys_.getMachine(parts[0]) == null)
+ for (String s : parts)
{
- String mname = parts[0].trim();
- for (String m : sys_.machineNames())
- {
- if (m.startsWith(mname)) candidates.add(new Candidate(m+"/"));
- }
+ if (s.startsWith(path)) candidates.add(new Candidate(s));
}
return;
diff --git a/src/main/java/com/viklauverk/eventbtools/core/Util.java b/src/main/java/com/viklauverk/eventbtools/core/Util.java
index c246851..a97eb53 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/Util.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/Util.java
@@ -233,10 +233,10 @@ public static String replaceEVBT(String template,
return out.toString();
}
- // Pattern Elevator -- render whole machine
- // Elevator/invariants -- render all invariants
- // Elevator/invariants/inv_space -- render only this invariant
-
+ // Pattern mch/Elevator -- render whole machine
+ // mch/Elevator/invariant -- render all invariants
+ // mch/Elevator/event/moveUp -- render event
+ // mch/Elevator/event/moveUp/guard/grd_1 -- render this guard only
public static boolean match(String path, String pattern)
{
log_match.trace("match? \"%s\" \"%s\"", path, pattern);
diff --git a/src/main/java/com/viklauverk/eventbtools/core/VisitContext.java b/src/main/java/com/viklauverk/eventbtools/core/VisitContext.java
index de3f6f6..1d0a624 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/VisitContext.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/VisitContext.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
@@ -24,7 +24,7 @@ public class VisitContext
*/
public static void walk(RenderContext rc, Context ctx, String pattern)
{
- boolean m = Util.match(ctx.name()+"/", pattern);
+ boolean m = Util.match(RenderContext.buildContextPartName(ctx), pattern);
if (m) rc.visit_ContextStart(ctx);
if (m && ctx.hasExtend())
@@ -41,12 +41,12 @@ public static void walk(RenderContext rc, Context ctx, String pattern)
if (ctx.hasSets())
{
- boolean s = Util.match(ctx.name()+"/sets/", pattern);
+ boolean s = Util.match(RenderContext.buildSetPartName(ctx, null), pattern);
if (s) rc.visit_SetsStart(ctx);
for (CarrierSet set : ctx.setOrdering())
{
- boolean ss = Util.match(ctx.name()+"/sets/"+set.name()+"/", pattern);
+ boolean ss = Util.match(RenderContext.buildSetPartName(ctx, set), pattern);
if (ss)
{
rc.visit_Set(ctx, set);
@@ -57,12 +57,12 @@ public static void walk(RenderContext rc, Context ctx, String pattern)
if (ctx.hasConstants())
{
- boolean c = Util.match(ctx.name()+"/constants/", pattern);
+ boolean c = Util.match(RenderContext.buildConstantPartName(ctx, null), pattern);
if (c) rc.visit_ConstantsStart(ctx);
for (Constant constant : ctx.constantOrdering())
{
- boolean cc = Util.match(ctx.name()+"/constants/"+constant.name()+"/", pattern);
+ boolean cc = Util.match(RenderContext.buildConstantPartName(ctx, constant), pattern);
if (cc) rc.visit_Constant(ctx, constant);
}
if (c) rc.visit_ConstantsEnd(ctx);
@@ -70,12 +70,12 @@ public static void walk(RenderContext rc, Context ctx, String pattern)
if (ctx.hasAxioms())
{
- boolean a = Util.match(ctx.name()+"/axioms/", pattern);
+ boolean a = Util.match(RenderContext.buildAxiomPartName(ctx, null), pattern);
if (a) rc.visit_AxiomsStart(ctx);
for (Axiom axi : ctx.axiomOrdering())
{
- boolean aa = Util.match(ctx.name()+"/axioms/"+axi.name()+"/", pattern);
+ boolean aa = Util.match(RenderContext.buildAxiomPartName(ctx, axi), pattern);
if (aa) rc.visit_Axiom(ctx, axi);
}
if (a) rc.visit_AxiomsEnd(ctx);
diff --git a/src/main/java/com/viklauverk/eventbtools/core/VisitEvent.java b/src/main/java/com/viklauverk/eventbtools/core/VisitEvent.java
index 3d35869..0fed56c 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/VisitEvent.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/VisitEvent.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
@@ -26,8 +26,7 @@ public class VisitEvent
{
public static void walk(RenderEvent re, Event e, String pattern)
{
- String path = e.machine().name()+"/events/"+e.name()+"/";
- boolean m = Util.match(path, pattern);
+ boolean m = Util.match(RenderEvent.buildEventPartName(e), pattern);
if (m) re.visit_EventStart(e);
@@ -55,7 +54,7 @@ public static void walk(RenderEvent re, Event e, String pattern)
if (m) re.visit_ParametersStart(e);
for (Variable par : e.parameterOrdering())
{
- boolean pp = Util.match(path+"parameters/"+par.name()+"/", pattern);
+ boolean pp = Util.match(RenderEvent.buildParameterPartName(e, par), pattern);
if (pp) re.visit_Parameter(e, par);
}
if (m) re.visit_ParametersEnd(e);
@@ -66,17 +65,18 @@ public static void walk(RenderEvent re, Event e, String pattern)
if (m) re.visit_GuardsStart(e);
for (Guard gua : e.guardOrdering())
{
- boolean gg = Util.match(path+"guards/"+gua.name()+"/", pattern);
+ boolean gg = Util.match(RenderEvent.buildGuardPartName(e, gua), pattern);
if (gg) re.visit_Guard(e, gua);
}
if (m) re.visit_GuardsEnd(e);
}
+
if (e.hasWitnesses())
{
if (m) re.visit_WitnessesStart(e);
for (Witness wit : e.witnessOrdering())
{
- boolean ww = Util.match(path+"witnesses/"+wit.name()+"/", pattern);
+ boolean ww = Util.match(RenderEvent.buildWitnessPartName(e, wit), pattern);
if (ww) re.visit_Witness(e, wit);
}
if (m) re.visit_WitnessesEnd(e);
@@ -87,7 +87,7 @@ public static void walk(RenderEvent re, Event e, String pattern)
if (m) re.visit_ActionsStart(e);
for (Action act : e.actionOrdering())
{
- boolean aa = Util.match(path+"actions/"+act.name()+"/", pattern);
+ boolean aa = Util.match(RenderEvent.buildActionPartName(e, act), pattern);
if (aa) re.visit_Action(e, act);
}
if (m) re.visit_ActionsEnd(e);
diff --git a/src/main/java/com/viklauverk/eventbtools/core/VisitMachine.java b/src/main/java/com/viklauverk/eventbtools/core/VisitMachine.java
index 587aec9..2cec9d7 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/VisitMachine.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/VisitMachine.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,7 +21,7 @@ public class VisitMachine
{
public static void walk(RenderMachine v, Machine mch, String pattern)
{
- boolean m = Util.match(mch.name()+"/", pattern);
+ boolean m = Util.match(RenderMachine.buildMachinePartName(mch), pattern);
if (m) v.visit_MachineStart(mch);
@@ -46,12 +46,12 @@ public static void walk(RenderMachine v, Machine mch, String pattern)
if (mch.hasVariables())
{
- boolean vs = Util.match(mch.name()+"/variables/", pattern);
+ boolean vs = Util.match(RenderMachine.buildMachineVariablePartName(mch, null), pattern);
if (vs) v.visit_VariablesStart(mch);
for (Variable var : mch.variableOrdering())
{
- boolean vv = Util.match(mch.name()+"/variables/"+var.name()+"/", pattern);
+ boolean vv = Util.match(RenderMachine.buildMachineVariablePartName(mch, var), pattern);
if (vv) v.visit_Variable(mch, var);
}
if (vs) v.visit_VariablesEnd(mch);
@@ -59,12 +59,12 @@ public static void walk(RenderMachine v, Machine mch, String pattern)
if (mch.hasInvariants())
{
- boolean i = Util.match(mch.name()+"/invariants/", pattern);
+ boolean i = Util.match(RenderMachine.buildMachineInvariantPartName(mch, null), pattern);
if (i) v.visit_InvariantsStart(mch);
for (Invariant inv : mch.invariantOrdering())
{
- boolean ii = Util.match(mch.name()+"/invariants/"+inv.name()+"/", pattern);
+ boolean ii = Util.match(RenderMachine.buildMachineInvariantPartName(mch, inv), pattern);
if (ii) v.visit_Invariant(mch, inv);
}
if (i) v.visit_InvariantsEnd(mch);
@@ -72,12 +72,12 @@ public static void walk(RenderMachine v, Machine mch, String pattern)
if (mch.hasVariants())
{
- boolean vs = Util.match(mch.name()+"/variants/", pattern);
+ boolean vs = Util.match(RenderMachine.buildMachineVariantPartName(mch, null), pattern);
if (vs) v.visit_VariantsStart(mch);
for (Variant var : mch.variantOrdering())
{
- boolean vv = Util.match(mch.name()+"/variants/"+var.name()+"/", pattern);
+ boolean vv = Util.match(RenderMachine.buildMachineVariantPartName(mch, var), pattern);
if (vv) v.visit_Variant(mch, var);
}
if (vs) v.visit_VariantsEnd(mch);
@@ -85,26 +85,11 @@ public static void walk(RenderMachine v, Machine mch, String pattern)
if (mch.hasEvents())
{
- String name = mch.name()+"/events/";
- boolean e = Util.match(name, pattern);
+ boolean e = Util.match("mch/"+mch.name()+"/event/", pattern);
if (e) v.visit_EventsStart(mch);
for (Event eve : mch.eventOrdering())
{
- /*
- String p = pattern;
- if (p.equals(name) || p.equals(mch.name()))
- {
- p = "";
- }
- else if (p.length() > name.length())
- {
- // The pattern is Elevator/events/moveDown/grd0_1
- // cut the pattern to just moveDown/grd0_1 so that it works
- // within the event visitor.
- p = p.substring(name.length()+1);
- }
- */
v.visit_Event(mch, eve, pattern);
}
if (e) v.visit_EventsEnd(mch);
diff --git a/src/main/java/com/viklauverk/eventbtools/core/VisitPolymorphicDataType.java b/src/main/java/com/viklauverk/eventbtools/core/VisitPolymorphicDataType.java
index a4e50d0..c8f3ef0 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/VisitPolymorphicDataType.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/VisitPolymorphicDataType.java
@@ -26,8 +26,7 @@ public class VisitPolymorphicDataType
{
public static void walk(RenderPolymorphicDataType re, PolymorphicDataType pdt, String pattern)
{
- String path = pdt.theory().name()+"/datatypes/"+pdt.baseName()+"/";
- boolean m = Util.match(path, pattern);
+ boolean m = Util.match(RenderPolymorphicDataType.buildPolymorphicDataTypePartName(pdt), pattern);
if (m) re.visit_PolymorphicDataTypeStart(pdt);
@@ -38,7 +37,7 @@ public static void walk(RenderPolymorphicDataType re, PolymorphicDataType pdt, S
if (m) re.visit_ConstructorsStart(pdt);
for (Constructor cnstr : pdt.constructorOrdering())
{
- boolean pp = Util.match(path+"constructors/"+cnstr.name()+"/", pattern);
+ boolean pp = Util.match(RenderPolymorphicDataType.buildConstructorPartName(pdt, cnstr), pattern);
if (pp) re.visit_Constructor(pdt, cnstr);
}
if (m) re.visit_ConstructorsEnd(pdt);
diff --git a/src/main/java/com/viklauverk/eventbtools/core/VisitTheory.java b/src/main/java/com/viklauverk/eventbtools/core/VisitTheory.java
index 982c989..7ecd295 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/VisitTheory.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/VisitTheory.java
@@ -24,7 +24,7 @@ public class VisitTheory
*/
public static void walk(RenderTheory rt, Theory thr, String pattern)
{
- boolean m = Util.match(thr.name()+"/", pattern);
+ boolean m = Util.match(RenderTheory.buildTheoryPartName(thr), pattern);
if (m) rt.visit_TheoryStart(thr);
if (m && thr.hasImports())
@@ -41,12 +41,12 @@ public static void walk(RenderTheory rt, Theory thr, String pattern)
if (thr.hasPolymorphicDataTypes())
{
- boolean s = Util.match(thr.name()+"/datatypes/", pattern);
+ boolean s = Util.match(RenderTheory.buildDataTypePartName(thr, null), pattern);
if (s) rt.visit_PolymorphicDataTypesStart(thr);
for (PolymorphicDataType pdt : thr.polymorphicDataTypeOrdering())
{
- boolean ss = Util.match(thr.name()+"/datatypes/"+pdt.baseName()+"/", pattern);
+ boolean ss = Util.match(RenderTheory.buildDataTypePartName(thr, pdt), pattern);
if (ss)
{
rt.visit_PolymorphicDataType(thr, pdt);
@@ -57,12 +57,12 @@ public static void walk(RenderTheory rt, Theory thr, String pattern)
if (thr.hasOperators())
{
- boolean s = Util.match(thr.name()+"/operators/", pattern);
+ boolean s = Util.match(RenderTheory.buildOperatorPartName(thr, null), pattern);
if (s) rt.visit_OperatorsStart(thr);
for (Operator oprt : thr.operatorOrdering())
{
- boolean ss = Util.match(thr.name()+"/operator/"+oprt.name()+"/", pattern);
+ boolean ss = Util.match(RenderTheory.buildOperatorPartName(thr, oprt), pattern);
if (ss)
{
rt.visit_Operator(thr, oprt);
diff --git a/src/main/java/com/viklauverk/eventbtools/core/cmd/CmdEbShowPart.java b/src/main/java/com/viklauverk/eventbtools/core/cmd/CmdEbShowPart.java
index a0bba39..e7b91e0 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/cmd/CmdEbShowPart.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/cmd/CmdEbShowPart.java
@@ -46,12 +46,7 @@ public String go()
return unknownOptions();
}
- String pattern = line_;
- if (!pattern.startsWith("*"))
- {
- // Force the pattern to match all to the end of the path.
- pattern += "/";
- }
+ String pattern = line_.trim();
RenderTarget rt = toRenderTarget(render_plain, render_terminal, render_tex, render_html, console_.renderTarget());
RenderAttributes ra = console_.renderAttributes().copy();
diff --git a/src/main/java/com/viklauverk/eventbtools/core/cmd/CmdSysLsParts.java b/src/main/java/com/viklauverk/eventbtools/core/cmd/CmdSysLsParts.java
index ca8b1e9..be91dc8 100644
--- a/src/main/java/com/viklauverk/eventbtools/core/cmd/CmdSysLsParts.java
+++ b/src/main/java/com/viklauverk/eventbtools/core/cmd/CmdSysLsParts.java
@@ -32,18 +32,11 @@ public CmdSysLsParts(Console console, String line)
public String go()
{
String part = line_.trim();
- try
- {
- List parts = console_.sys().listParts(part);
- StringBuilder sb = new StringBuilder();
- for (String p : parts) {
- sb.append(p+"\n");
- }
- return sb.toString();
- }
- catch (Exception e)
- {
- return e.getMessage();
+ List parts = console_.sys().listParts(part);
+ StringBuilder sb = new StringBuilder();
+ for (String p : parts) {
+ sb.append(p+"\n");
}
+ return sb.toString();
}
}
diff --git a/tests/test_docmod.sh b/tests/test_docmod.sh
index ad7d8fd..33fb89a 100755
--- a/tests/test_docmod.sh
+++ b/tests/test_docmod.sh
@@ -20,7 +20,7 @@ EVBT(eb.show.formula --plain x:BOOL & y:S => E = F)
+++++
EVBT(sys.read models/Elevator)
+++++
-EVBT(eb.show.part --frame --plain Elevator/events/enterDest/guards/grd_1)
+EVBT(eb.show.part --frame --plain mch/Elevator/event/enterDest/guard/grd_1)
+++++
END
EOF