From ca8acac1d6d0103e3952a37c022efd1a9376851c Mon Sep 17 00:00:00 2001 From: Michael Kirsten Date: Thu, 21 Sep 2023 06:04:31 +0200 Subject: [PATCH 1/4] First investigation results --- virage/pom.xml | 2 +- .../virage/isabelle/IsabelleProofChecker.java | 51 ++++++++++++------- .../virage/isabelle/ScalaIsabelleFacade.java | 2 +- .../main/resources/voting_context.template | 4 +- 4 files changed, 36 insertions(+), 23 deletions(-) diff --git a/virage/pom.xml b/virage/pom.xml index 8011f17..3166fa0 100644 --- a/virage/pom.xml +++ b/virage/pom.xml @@ -387,7 +387,7 @@ org.codehaus.mojo versions-maven-plugin - 2.16.0 + 2.16.1 file:///${basedir}/rules.xml false diff --git a/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/IsabelleProofChecker.java b/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/IsabelleProofChecker.java index e25b05f..0365c7a 100644 --- a/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/IsabelleProofChecker.java +++ b/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/IsabelleProofChecker.java @@ -148,6 +148,16 @@ public final class IsabelleProofChecker { */ private static final String PWD_CMD = "`pwd`"; + /** + * The prefix for ad-hoc Isabelle sessions. + */ + private static final String AD_HOC_SESSION_PREFIX = "ad_hoc_session_"; + + /** + * The pattern for simple date formats, intended for creating quasi unique file names. + */ + private static final String DATE_FORMAT_PATTERN = "yyyyMMddHHmmss"; + /** * The session name variable. */ @@ -321,7 +331,8 @@ private String buildSessionRoot(final String theoryName, final File theory) { // rebuilding single sessions without triggering full rebuilds. // TODO: Is there a way to do it? final String localSessionName = - "ad_hoc_session_" + new SimpleDateFormat("yyyyMMddHHmmss").format(new Date()); + AD_HOC_SESSION_PREFIX + + new SimpleDateFormat(DATE_FORMAT_PATTERN).format(new Date()); String result = this.rootTemplate .replace(SESSION_NAME_VAR, localSessionName).replace(THEORY_NAME_VAR, theoryName); result = result.replace(PARENT_NAME_VAR, this.parentName); @@ -575,24 +586,26 @@ public Pair verifyTheoryFile(final File theory, + "by employing different solvers."); final String errors = this.lastEvent.getValue("errors"); - command = "purge_theories " + sessionAndTheoriesCommand; - this.sendCommandAndWaitForOk(command); - final Pattern pattern = Pattern.compile("line=[0-9]+"); - final Matcher matcher = pattern.matcher(errors); - - if (matcher.find()) { - final String line = errors.substring(matcher.start(), matcher.end()); - // Isabelle starts counting at 1. - final int lineNum = Integer.parseInt(line.split("=")[1]) - 1; - final File newFile = this.replaceSolver(theory, lineNum); - if (newFile != null) { - // The content of the file has changed, and this can - // only happen IsabelleUtils.SOLVERS.length times, - // so the recursive call is fine. - return this.verifyTheoryFile(newFile, framework); - } else { - LOGGER.info("Automatic verification failed. " - + "You might be able to fix the errors manually within Isabelle."); + if (errors != null) { + command = "purge_theories " + sessionAndTheoriesCommand; + this.sendCommandAndWaitForOk(command); + final Pattern pattern = Pattern.compile("line=[0-9]+"); + final Matcher matcher = pattern.matcher(errors); + + if (matcher.find()) { + final String line = errors.substring(matcher.start(), matcher.end()); + // Isabelle starts counting at 1. + final int lineNum = Integer.parseInt(line.split("=")[1]) - 1; + final File newFile = this.replaceSolver(theory, lineNum); + if (newFile != null) { + // The content of the file has changed, and this can + // only happen IsabelleUtils.SOLVERS.length times, + // so the recursive call is fine. + return this.verifyTheoryFile(newFile, framework); + } else { + LOGGER.info("Automatic verification failed. " + + "You might be able to fix the errors manually within Isabelle."); + } } } return new Pair(false, null); diff --git a/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/ScalaIsabelleFacade.java b/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/ScalaIsabelleFacade.java index 5fb4579..7c74696 100644 --- a/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/ScalaIsabelleFacade.java +++ b/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/ScalaIsabelleFacade.java @@ -155,7 +155,7 @@ public final class ScalaIsabelleFacade { * The theory-name function. */ private static final String THY_NAME = - "Context" + IsabelleUtils.THEORY_NAME_SEPARATOR + "theory_name"; + "Context" + IsabelleUtils.THEORY_NAME_SEPARATOR + "theory_base_name"; /** * The specifications-of function. diff --git a/virage/src/main/resources/voting_context.template b/virage/src/main/resources/voting_context.template index 41f1db2..fbac216 100644 --- a/virage/src/main/resources/voting_context.template +++ b/virage/src/main/resources/voting_context.template @@ -4,9 +4,9 @@ import scala.language.postfixOps import scala.io.Source /* ENUM -class Bounded[A](entities: List[A]) extends Enum.`enum`[A] { +class Bounded[A](entities: List[A]) extends Enum.`enuma`[A] { - val `Enum.enum`: List[A] = entities + val `Enum.enuma`: List[A] = entities val `Enum.enum_all`: (A => Boolean) => Boolean = (p => entities.forall(p)) From 25e78c1d38a3e6f4c7de457b5cb3028179318299 Mon Sep 17 00:00:00 2001 From: Michael Kirsten Date: Mon, 25 Sep 2023 20:00:23 +0200 Subject: [PATCH 2/4] Made code and proof generation work for simple voting rules, still need to inspect more complex ones --- virage/.gitignore | 5 + .../kit/kastel/formal/util/StringUtils.java | 43 + .../formal/virage/beast/CCodeGenerator.java | 4 +- .../core/VirageCommandLineInterface.java | 6 +- .../isabelle/IsabelleCodeGenerator.java | 36 +- .../isabelle/IsabelleFrameworkExtractor.java | 20 +- .../isabelle/IsabelleTheoryGenerator.java | 49 +- .../formal/virage/isabelle/IsabelleUtils.java | 15 + .../virage/isabelle/ScalaIsabelleFacade.java | 2 +- .../jobs/VirageAnalyzeAllPropertiesJob.java | 6 +- .../jobs/VirageIsabelleGenerateScalaJob.java | 3 +- .../formal/virage/types/CompositionProof.java | 18 +- .../resources/c_implementations/wrapper.c | 4 +- virage/src/main/resources/code_file.template | 2 +- .../formal/beast/highlevel/javafx/BEAST.fxml | 16 +- .../javafx/bundles/LangBundle_de.properties | 4 +- .../javafx/bundles/LangBundle_en.properties | 4 +- .../main/resources/voting_context.template | 54 +- .../resources/c_implementations/wrapper.c | 4 +- virage/src/test/resources/instances/README.md | 4 +- .../output/document/Aggregator.tex | 159 - .../output/document/Blacks_Rule.tex | 111 - .../output/document/Borda_Module.tex | 131 - .../output/document/Borda_Rule.tex | 116 - .../output/document/Classic_Nanson_Rule.tex | 117 - .../output/document/Condorcet_Module.tex | 275 -- .../output/document/Copeland_Module.tex | 917 ---- .../output/document/Copeland_Rule.tex | 179 - .../output/document/Defer_Equal_Condition.tex | 101 - .../output/document/Defer_Module.tex | 222 - .../document/Defer_One_Loop_Composition.tex | 130 - .../document/Drop_And_Pass_Compatibility.tex | 459 -- .../output/document/Drop_Module.tex | 358 -- .../output/document/Elect_Composition.tex | 1049 ---- .../output/document/Elect_Module.tex | 190 - .../output/document/Electoral_Module.tex | 3358 ------------- .../output/document/Elimination_Module.tex | 1358 ------ .../output/document/Evaluation_Function.tex | 344 -- .../output/document/Loop_Composition.tex | 2502 ---------- .../output/document/Maximum_Aggregator.tex | 561 --- .../document/Maximum_Parallel_Composition.tex | 1960 -------- .../output/document/Minimax_Module.tex | 690 --- .../output/document/Minimax_Rule.tex | 177 - .../output/document/Nanson_Baldwin_Rule.tex | 113 - .../document/Pairwise_Majority_Rule.tex | 197 - .../output/document/Parallel_Composition.tex | 412 -- .../output/document/Pass_Module.tex | 1466 ------ .../output/document/Plurality_Module.tex | 1263 ----- .../output/document/Preference_Relation.tex | 4290 ----------------- .../old_theories/output/document/Profile.tex | 1906 -------- .../old_theories/output/document/Result.tex | 469 -- .../output/document/Revision_Composition.tex | 470 -- .../output/document/Schwartz_Rule.tex | 115 - .../document/Sequential_Composition.tex | 3359 ------------- .../Sequential_Majority_Comparison.tex | 1331 ----- .../output/document/Termination_Condition.tex | 99 - .../old_theories/output/document/comment.sty | 278 -- .../old_theories/output/document/isabelle.sty | 267 - .../output/document/isabellesym.sty | 427 -- .../output/document/isabelletags.sty | 1 - .../old_theories/output/document/pdfsetup.sty | 7 - .../output/document/railsetup.sty | 1202 ----- .../old_theories/output/document/root.bib | 71 - .../old_theories/output/document/root.tex | 56 - .../old_theories/output/document/session.tex | 36 - .../old_theories/output/document/settings.tex | 30 - .../Basic_Modules/Plurality_Module.thy | 19 - .../#Preference_Relation.thy# | 1115 ----- .../Social_Choice_Types/#Profile.thy# | 853 ---- .../theories/output/document/Aggregator.tex | 133 - .../output/document/Aggregator_Facts.tex | 258 - .../output/document/Aggregator_Properties.tex | 74 - .../theories/output/document/Blacks_Rule.tex | 103 - .../theories/output/document/Borda_Rule.tex | 110 - .../output/document/Classic_Nanson_Rule.tex | 107 - .../Composite_Elimination_Modules.tex | 1019 ---- .../output/document/Composite_Structures.tex | 1266 ----- .../output/document/Condorcet_Consistency.tex | 63 - .../output/document/Condorcet_Facts.tex | 795 --- .../output/document/Condorcet_Properties.tex | 93 - .../output/document/Condorcet_Rules.tex | 1954 -------- .../output/document/Copeland_Rule.tex | 162 - .../output/document/Defer_Equal_Condition.tex | 101 - .../theories/output/document/Defer_Module.tex | 150 - .../document/Disjoint_Compatibility.tex | 70 - .../document/Disjoint_Compatibility_Facts.tex | 275 -- .../document/Disjoint_Compatibility_Rules.tex | 521 -- .../theories/output/document/Drop_Module.tex | 272 -- .../theories/output/document/Elect_Module.tex | 147 - .../output/document/Electoral_Module.tex | 1952 -------- .../output/document/Elimination_Module.tex | 596 --- .../output/document/Evaluation_Function.tex | 97 - .../theories/output/document/Homogeneity.tex | 69 - .../theories/output/document/Indep_Of_Alt.tex | 60 - .../output/document/Loop_Composition.tex | 806 ---- .../output/document/Maximum_Aggregator.tex | 343 -- .../theories/output/document/Minimax_Rule.tex | 160 - .../output/document/Monotonicity_Facts.tex | 923 ---- .../document/Monotonicity_Properties.tex | 108 - .../output/document/Monotonicity_Rules.tex | 2710 ----------- .../output/document/Nanson_Baldwin_Rule.tex | 103 - .../document/Pairwise_Majority_Rule.tex | 195 - .../output/document/Parallel_Composition.tex | 214 - .../theories/output/document/Pass_Module.tex | 270 -- .../output/document/Plurality_Module.tex | 257 - .../output/document/Preference_Relation.tex | 4290 ----------------- .../theories/output/document/Profile.tex | 2959 ------------ .../theories/output/document/Result.tex | 469 -- .../theories/output/document/Result_Facts.tex | 2293 --------- .../output/document/Result_Properties.tex | 350 -- .../theories/output/document/Result_Rules.tex | 2466 ---------- .../output/document/Revision_Composition.tex | 233 - .../output/document/Schwartz_Rule.tex | 107 - .../document/Sequential_Composition.tex | 1373 ------ .../Sequential_Majority_Comparison.tex | 1341 ------ .../output/document/Termination_Condition.tex | 99 - .../output/document/Weak_Monotonicity.tex | 62 - .../theories/output/document/comment.sty | 278 -- .../theories/output/document/isabelle.sty | 267 - .../theories/output/document/isabellesym.sty | 427 -- .../theories/output/document/isabelletags.sty | 1 - .../theories/output/document/pdfsetup.sty | 7 - .../theories/output/document/railsetup.sty | 1202 ----- .../theories/output/document/root.bib | 71 - .../theories/output/document/root.tex | 56 - .../theories/output/document/session.tex | 48 - .../theories/output/document/settings.tex | 30 - 127 files changed, 184 insertions(+), 70396 deletions(-) delete mode 100644 virage/src/test/resources/old_theories/output/document/Aggregator.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Blacks_Rule.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Borda_Module.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Borda_Rule.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Classic_Nanson_Rule.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Condorcet_Module.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Copeland_Module.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Copeland_Rule.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Defer_Equal_Condition.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Defer_Module.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Defer_One_Loop_Composition.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Drop_And_Pass_Compatibility.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Drop_Module.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Elect_Composition.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Elect_Module.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Electoral_Module.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Elimination_Module.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Evaluation_Function.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Loop_Composition.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Maximum_Aggregator.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Maximum_Parallel_Composition.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Minimax_Module.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Minimax_Rule.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Nanson_Baldwin_Rule.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Pairwise_Majority_Rule.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Parallel_Composition.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Pass_Module.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Plurality_Module.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Preference_Relation.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Profile.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Result.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Revision_Composition.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Schwartz_Rule.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Sequential_Composition.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Sequential_Majority_Comparison.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/Termination_Condition.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/comment.sty delete mode 100644 virage/src/test/resources/old_theories/output/document/isabelle.sty delete mode 100644 virage/src/test/resources/old_theories/output/document/isabellesym.sty delete mode 100644 virage/src/test/resources/old_theories/output/document/isabelletags.sty delete mode 100644 virage/src/test/resources/old_theories/output/document/pdfsetup.sty delete mode 100644 virage/src/test/resources/old_theories/output/document/railsetup.sty delete mode 100644 virage/src/test/resources/old_theories/output/document/root.bib delete mode 100644 virage/src/test/resources/old_theories/output/document/root.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/session.tex delete mode 100644 virage/src/test/resources/old_theories/output/document/settings.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/Social_Choice_Types/#Preference_Relation.thy# delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/Social_Choice_Types/#Profile.thy# delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Aggregator.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Aggregator_Facts.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Aggregator_Properties.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Blacks_Rule.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Borda_Rule.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Classic_Nanson_Rule.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Composite_Elimination_Modules.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Composite_Structures.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Condorcet_Consistency.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Condorcet_Facts.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Condorcet_Properties.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Condorcet_Rules.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Copeland_Rule.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Defer_Equal_Condition.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Defer_Module.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Disjoint_Compatibility.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Disjoint_Compatibility_Facts.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Disjoint_Compatibility_Rules.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Drop_Module.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Elect_Module.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Electoral_Module.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Elimination_Module.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Evaluation_Function.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Homogeneity.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Indep_Of_Alt.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Loop_Composition.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Maximum_Aggregator.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Minimax_Rule.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Monotonicity_Facts.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Monotonicity_Properties.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Monotonicity_Rules.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Nanson_Baldwin_Rule.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Pairwise_Majority_Rule.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Parallel_Composition.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Pass_Module.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Plurality_Module.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Preference_Relation.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Profile.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Result.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Result_Facts.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Result_Properties.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Result_Rules.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Revision_Composition.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Schwartz_Rule.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Sequential_Composition.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Sequential_Majority_Comparison.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Termination_Condition.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/Weak_Monotonicity.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/comment.sty delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/isabelle.sty delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/isabellesym.sty delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/isabelletags.sty delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/pdfsetup.sty delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/railsetup.sty delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/root.bib delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/root.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/session.tex delete mode 100644 virage/src/test/resources/verifiedVotingRuleConstruction/theories/output/document/settings.tex diff --git a/virage/.gitignore b/virage/.gitignore index 5216f15..0f6ca3f 100644 --- a/virage/.gitignore +++ b/virage/.gitignore @@ -4,4 +4,9 @@ /.classpath /.project /.settings/ +/.bloop/ +/.metals/ +/.vscode/ /src/main/resources/generated/ +/.apt_generated/ +/.apt_generated_tests/ diff --git a/virage/src/main/java/edu/kit/kastel/formal/util/StringUtils.java b/virage/src/main/java/edu/kit/kastel/formal/util/StringUtils.java index 2e4e9fd..c151a63 100644 --- a/virage/src/main/java/edu/kit/kastel/formal/util/StringUtils.java +++ b/virage/src/main/java/edu/kit/kastel/formal/util/StringUtils.java @@ -122,6 +122,16 @@ public final class StringUtils { */ public static final int TEN = 10; + /** + * An opening bracket sign. + */ + private static final String OPENING_BRACKET = "]"; + + /** + * A closing bracket sign. + */ + private static final String CLOSING_BRACKET = "["; + /** * The disjunction (or) sign. */ @@ -372,6 +382,39 @@ public static String parenthesize2(final String... args) { return OPENING_PARENTHESIS + printCollection2(Arrays.asList(args)) + CLOSING_PARENTHESIS; } + /** + * Puts brackets around a comma-separated list of strings. + * + * @param args the string arguments to bracketize + * @return the bracketized string representation + */ + public static String bracketize(final String... args) { + return OPENING_BRACKET + printCollection(Arrays.asList(args)) + CLOSING_BRACKET; + } + + /** + * Puts parentheses around a comma-separated list of strings. + * + * @param args the string arguments to bracketize + * @return the bracketized string representation + */ + public static String bracketize(final Collection args) { + if (args == null || args.isEmpty()) { + return EMPTY; + } + return bracketize(args.toArray(new String[args.size()])); + } + + /** + * Puts brackets around a space-separated list of strings. + * + * @param args the string arguments to bracketize + * @return the bracketized string representation + */ + public static String bracketize2(final String... args) { + return OPENING_BRACKET + printCollection2(Arrays.asList(args)) + CLOSING_BRACKET; + } + /** * Returns function string with a variable amount of argument. * diff --git a/virage/src/main/java/edu/kit/kastel/formal/virage/beast/CCodeGenerator.java b/virage/src/main/java/edu/kit/kastel/formal/virage/beast/CCodeGenerator.java index 4c5059c..c0623c0 100644 --- a/virage/src/main/java/edu/kit/kastel/formal/virage/beast/CCodeGenerator.java +++ b/virage/src/main/java/edu/kit/kastel/formal/virage/beast/CCodeGenerator.java @@ -267,7 +267,7 @@ private List findMissingTemplates(final DecompositionTree composition, /*public File generateAndCompileCCodeFromComposition(final String compositionString, final int numVoters, - final int numCandidates) + final int numAlternatives) throws IOException, InterruptedException, CompilationFailedException { final File votingRuleFile = this.getCCodeFromComposition(compositionString); String cFiles = StringUtils.EMPTY; @@ -293,7 +293,7 @@ private List findMissingTemplates(final DecompositionTree composition, final String gccCommand = ConfigReader.getInstance().getGccExecutable() + StringUtils.prefixSpace(tmpVotingRuleFile.getAbsolutePath()) + cFiles + " -o " + exeFile.getAbsolutePath() + " -D V=" + numVoters - + " -D C=" + numCandidates; + + " -D C=" + numAlternatives; final Pair output = ProcessUtils.runTerminatingProcess(gccCommand); if (!output.getFirstValue().isEmpty()) { LOGGER.warn(output.getFirstValue()); diff --git a/virage/src/main/java/edu/kit/kastel/formal/virage/core/VirageCommandLineInterface.java b/virage/src/main/java/edu/kit/kastel/formal/virage/core/VirageCommandLineInterface.java index e5fd323..1882a83 100644 --- a/virage/src/main/java/edu/kit/kastel/formal/virage/core/VirageCommandLineInterface.java +++ b/virage/src/main/java/edu/kit/kastel/formal/virage/core/VirageCommandLineInterface.java @@ -551,12 +551,10 @@ public String requestString(final String message) { this.displayInputMarker(); final String input = this.scanner.nextLine(); switch (input) { - case StringUtils.QUESTION: - case "h": - case HELP: + case StringUtils.QUESTION, "h", "H", HELP: this.displayHelp(); break; - case EXIT: + case "x", "X", "q", "Q", EXIT: this.core.submit(new VirageExitJob(this, 0)); break; default: diff --git a/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/IsabelleCodeGenerator.java b/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/IsabelleCodeGenerator.java index 0b24c14..2dd2f3f 100644 --- a/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/IsabelleCodeGenerator.java +++ b/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/IsabelleCodeGenerator.java @@ -131,11 +131,6 @@ public final class IsabelleCodeGenerator { */ private static final String PARENT_NAME_VAR = "$PARENT_NAME"; - /** - * String for enumerable. - */ - private static final String ENUM = "Enum"; - /** * Comment for enumerable. */ @@ -158,9 +153,11 @@ public final class IsabelleCodeGenerator { private static final String RELATION = StringUtils.parenthesize2( ScalaIsabelleFacade.DEFAULT_VARIABLE + StringUtils.COLON, - IsabelleUtils.SET + IsabelleUtils.THEORY_NAME_SEPARATOR + "set[" - + StringUtils.parenthesize(IsabelleUtils.DEFAULT_SET, IsabelleUtils.DEFAULT_SET) - + "]") + StringUtils.COLON; + IsabelleUtils.SET + IsabelleUtils.THEORY_NAME_SEPARATOR + IsabelleUtils.SET_FUNC + + StringUtils.bracketize( + StringUtils.parenthesize( + IsabelleUtils.DEFAULT_SET, IsabelleUtils.DEFAULT_SET))) + + StringUtils.COLON; /** * Option1 comment. @@ -410,7 +407,7 @@ private File prepareVotingContext(final String theoryName, final String moduleNa String result = IsabelleCodeGenerator.votingContextTemplate .replace(THEORY_NAME_VAR, theoryName).replace(MODULE_NAME_VAR, moduleName); - final boolean containsEnum = code.contains(ENUM); + final boolean containsEnum = code.contains(IsabelleUtils.ENUM); final boolean containsEquality = code.contains(EQUALITY); final boolean requiresRelation = code.contains(RELATION); final List parameters = new LinkedList(); @@ -423,7 +420,7 @@ private File prepareVotingContext(final String theoryName, final String moduleNa if (containsEquality) { result = result.replace(COMMENT_OPEN + EQUALITY_COMMENT, StringUtils.EMPTY) .replace(EQUALITY_COMMENT + COMMENT_CLOSE, StringUtils.EMPTY); - parameters.add(EQ_PARAMETER); + parameters.add(StringUtils.prefixSpace(EQ_PARAMETER)); } if (requiresRelation) { result = result.replace(COMMENT_OPEN + OPTION2_COMMENT, StringUtils.EMPTY) @@ -618,8 +615,10 @@ public File generateScalaCodeAndCompile(final File theory) theory.getName().length() - (IsabelleUtils.DOT_THY.length())); final String sessionName = this.buildSessionRoot(theoryName, theory); final File codeFile = invokeScalaCodeFromIsabelleTheory(theory, sessionName, theoryName); - // First, try using implicit values only - File votingContext = generateVotingContextFile(theoryName, moduleName, codeFile, false); + // First, try using implicit values only. + final File cxtImplVals = generateVotingContextFile(theoryName, moduleName, codeFile, false); + // If implicit values did not work, try setting them explicitly. + final File cxtExplVals = generateVotingContextFile(theoryName, moduleName, codeFile, true); final String jarPath = codeFile.getParent() + File.separator + moduleName + DOT_JAR; final String isaExec; try { @@ -627,10 +626,15 @@ public File generateScalaCodeAndCompile(final File theory) } catch (ExternalSoftwareUnavailableException e) { throw new CodeGenerationFailedException(e); } - int status = runScalaCompileProcess(codeFile, votingContext, isaExec, jarPath); - if (status != 0) { // Implicit values did not work, try setting them explicitly. - votingContext = generateVotingContextFile(theoryName, moduleName, codeFile, true); - status = runScalaCompileProcess(codeFile, votingContext, isaExec, jarPath); + int status = 1; + try { + status = runScalaCompileProcess(codeFile, cxtImplVals, isaExec, jarPath); + } catch (CodeGenerationFailedException e) { + LOGGER.info("Scala compilation with implicit values did not work," + + "now trying with explicit values."); + } + if (status != 0) { + status = runScalaCompileProcess(codeFile, cxtExplVals, isaExec, jarPath); if (status != 0) { throw new CodeGenerationFailedException( new CompilationFailedException( diff --git a/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/IsabelleFrameworkExtractor.java b/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/IsabelleFrameworkExtractor.java index ce4eecc..78072c0 100644 --- a/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/IsabelleFrameworkExtractor.java +++ b/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/IsabelleFrameworkExtractor.java @@ -334,16 +334,16 @@ public FrameworkRepresentation extract(final String sessionDir, final String ses changesMade = false; for (final PrologPredicate alias: toReturn.keySet()) { final List aliasExpansions = toReturn.get(alias); - for (final PrologPredicate candidate: toReturn.keySet()) { - if (candidate == alias) { + for (final PrologPredicate predicate: toReturn.keySet()) { + if (predicate == alias) { continue; } - final List candidateExpansions = toReturn.get(candidate); + final List predicateExpansions = toReturn.get(predicate); final List newValues = - computeAllExpansions(alias, aliasExpansions, candidateExpansions); + computeAllExpansions(alias, aliasExpansions, predicateExpansions); for (final PrologPredicate newValue: newValues) { - if (!candidateExpansions.contains(newValue)) { - candidateExpansions.add(newValue); + if (!predicateExpansions.contains(newValue)) { + predicateExpansions.add(newValue); changesMade = true; } } @@ -356,15 +356,15 @@ public FrameworkRepresentation extract(final String sessionDir, final String ses private static List computeAllExpansions(final PrologPredicate alias, final List aliasExpansions, - final List candidateExpansions) + final List predicateExpansions) throws ExternalSoftwareUnavailableException { final List toReturn = new LinkedList(); - for (final PrologPredicate candidateExpansion: candidateExpansions) { - final List children = candidateExpansion.getAllChildren(); + for (final PrologPredicate predicateExpansion: predicateExpansions) { + final List children = predicateExpansion.getAllChildren(); for (final PrologPredicate child: children) { if (child.getName().equals(alias.getName())) { for (final PrologPredicate aliasExpansion: aliasExpansions) { - toReturn.add(replaceAlias(candidateExpansion, child, aliasExpansion)); + toReturn.add(replaceAlias(predicateExpansion, child, aliasExpansion)); } } } diff --git a/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/IsabelleTheoryGenerator.java b/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/IsabelleTheoryGenerator.java index 5567d87..a66df73 100644 --- a/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/IsabelleTheoryGenerator.java +++ b/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/IsabelleTheoryGenerator.java @@ -5,9 +5,11 @@ import java.io.InputStream; import java.io.StringWriter; import java.nio.charset.StandardCharsets; +import java.util.ArrayList; import java.util.Collections; import java.util.HashMap; import java.util.HashSet; +import java.util.LinkedHashSet; import java.util.LinkedList; import java.util.List; import java.util.Map; @@ -269,26 +271,31 @@ private static String generateModuleParameterTypes(final List modulePara private static Pair buildModuleDef(final Map> moduleDefMap, final String importsParam, final String sessionName) { - String moduleDef = StringUtils.EMPTY; - final StringBuilder imports = new StringBuilder(importsParam); - // There will be only one iteration, but it is a bit tedious to extract - // single elements from sets. - for (final Map.Entry> entry: moduleDefMap.entrySet()) { - moduleDef = entry.getKey(); - // Additional imports might have occurred, which are only relevant - // for the definition of the module, but not used within the proofs. - // Add those. - for (final String importString: entry.getValue()) { - final String importStringWithoutSuffix = - importString.replace(IsabelleUtils.DOT_THY, StringUtils.EMPTY); - if (!imports.toString().contains(importStringWithoutSuffix)) { - final String importWithSuffix = - sessionName + StringUtils.PERIOD + importStringWithoutSuffix; - imports.append(StringUtils.surroundWithSpaces(importWithSuffix)); - } + final Set imports = new LinkedHashSet(); + imports.add(importsParam); + // There exists only one element, otherwise there is an exception thrown beforehand. + final String moduleDef = new ArrayList(moduleDefMap.keySet()).get(0); + // imports.add(sessionName + StringUtils.PERIOD + moduleDef); + // Additional imports might have occurred, which are only relevant + // for the definition of the module, but not used within the proofs. + // Add those. + for (final String importString: new ArrayList>(moduleDefMap.values()).get(0)) { + final String importStringWithoutSuffix = + importString.replace(IsabelleUtils.DOT_THY, StringUtils.EMPTY); + if (!imports.contains(importStringWithoutSuffix)) { + final String importWithSuffix = + sessionName + StringUtils.PERIOD + importStringWithoutSuffix; + imports.add(importWithSuffix); } } - return new Pair(moduleDef, imports.toString()); + // Build string from chain of imports + final StringBuilder importBuild = new StringBuilder(importsParam); + for (final String entry: imports) { + importBuild.append(StringUtils.surroundWithSpaces(entry)); + } + final String importString = + importBuild.toString().isBlank() ? IsabelleUtils.MAIN : importBuild.toString(); + return new Pair(moduleDef, importString); } private static String replaceVariables(final String theoryName, final String imports, @@ -356,16 +363,18 @@ public File generateTheoryFile(final String passedComposition, } final Pair moduleDefResult = buildModuleDef(moduleDefMap, imports, this.framework.getSessionName()); + if (moduleDefResult.getSecondValue().isBlank()) { + throw new IllegalArgumentException(); + } final StringBuilder proofsString = new StringBuilder(); for (final CompositionProof proof: proofs) { proofsString.append(this.generator.generateIsabelleProof(proof) + System.lineSeparator() + System.lineSeparator()); } - final String prfString = proofsString.toString(); final String fileContents = replaceVariables(theoryName, moduleDefResult.getSecondValue(), moduleParameterTypeString, moduleName, moduleParameterString, - moduleDefResult.getFirstValue(), prfString); + moduleDefResult.getFirstValue(), proofsString.toString()); final SimpleFileWriter writer = new SimpleFileWriter(); final String outputPath = buildOutputPath(passedOutputPath, theoryName); writer.writeToFile(outputPath, fileContents); diff --git a/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/IsabelleUtils.java b/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/IsabelleUtils.java index 52ade5f..d9fffe3 100644 --- a/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/IsabelleUtils.java +++ b/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/IsabelleUtils.java @@ -81,6 +81,11 @@ public final class IsabelleUtils { */ public static final String THEORY_NAME_SEPARATOR = StringUtils.PERIOD; + /** + * Main theory. + */ + public static final String MAIN = "Main"; + /** * Higher-order logic theory. */ @@ -91,6 +96,16 @@ public final class IsabelleUtils { */ public static final String SET = "Set"; + /** + * Isabelle's enumerable theory. + */ + public static final String ENUM = "Enum"; + + /** + * Isabelle's set function. + */ + public static final String SET_FUNC = "set"; + /** * String to represent the HOL type for natural numbers. */ diff --git a/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/ScalaIsabelleFacade.java b/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/ScalaIsabelleFacade.java index 7c74696..f89902b 100644 --- a/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/ScalaIsabelleFacade.java +++ b/virage/src/main/java/edu/kit/kastel/formal/virage/isabelle/ScalaIsabelleFacade.java @@ -155,7 +155,7 @@ public final class ScalaIsabelleFacade { * The theory-name function. */ private static final String THY_NAME = - "Context" + IsabelleUtils.THEORY_NAME_SEPARATOR + "theory_base_name"; + "Context" + IsabelleUtils.THEORY_NAME_SEPARATOR + "theory_long_name"; /** * The specifications-of function. diff --git a/virage/src/main/java/edu/kit/kastel/formal/virage/jobs/VirageAnalyzeAllPropertiesJob.java b/virage/src/main/java/edu/kit/kastel/formal/virage/jobs/VirageAnalyzeAllPropertiesJob.java index 377d70a..a2006b9 100644 --- a/virage/src/main/java/edu/kit/kastel/formal/virage/jobs/VirageAnalyzeAllPropertiesJob.java +++ b/virage/src/main/java/edu/kit/kastel/formal/virage/jobs/VirageAnalyzeAllPropertiesJob.java @@ -80,9 +80,9 @@ public final String presentConcreteResult() { protected final void concreteExecute() { this.unaryProperties = new LinkedList(); final VirageCore execCore = this.getExecutingCore(); - for (final Property candidate: execCore.getFrameworkRepresentation().getProperties()) { - if (!candidate.isAtomic() && candidate.getArity() == 1) { - this.unaryProperties.add(candidate); + for (final Property property: execCore.getFrameworkRepresentation().getProperties()) { + if (!property.isAtomic() && property.getArity() == 1) { + this.unaryProperties.add(property); } } Collections.sort(this.unaryProperties, diff --git a/virage/src/main/java/edu/kit/kastel/formal/virage/jobs/VirageIsabelleGenerateScalaJob.java b/virage/src/main/java/edu/kit/kastel/formal/virage/jobs/VirageIsabelleGenerateScalaJob.java index b9e72e7..12608c0 100644 --- a/virage/src/main/java/edu/kit/kastel/formal/virage/jobs/VirageIsabelleGenerateScalaJob.java +++ b/virage/src/main/java/edu/kit/kastel/formal/virage/jobs/VirageIsabelleGenerateScalaJob.java @@ -30,9 +30,8 @@ public final class VirageIsabelleGenerateScalaJob extends VirageJobWithExplicitR * @param compositionValue the composition */ public VirageIsabelleGenerateScalaJob(final VirageUserInterface issuer, - final String compositionValue) { + final String compositionValue) { super(issuer); - this.composition = compositionValue; } diff --git a/virage/src/main/java/edu/kit/kastel/formal/virage/types/CompositionProof.java b/virage/src/main/java/edu/kit/kastel/formal/virage/types/CompositionProof.java index 9b24ba4..3a0aaae 100644 --- a/virage/src/main/java/edu/kit/kastel/formal/virage/types/CompositionProof.java +++ b/virage/src/main/java/edu/kit/kastel/formal/virage/types/CompositionProof.java @@ -36,29 +36,27 @@ public final class CompositionProof { private String id = StringUtils.EMPTY; /** - * Simple constructor for a terminal proof step. + * Simple constructor. * * @param goalValue the goal + * @param subgoalsValue the subgoals * @param ruleValue the rule */ - public CompositionProof(final String goalValue, final CompositionRule ruleValue) { + public CompositionProof(final String goalValue, final List subgoalsValue, + final CompositionRule ruleValue) { this.goal = goalValue; - this.subgoals = new LinkedList(); + this.subgoals = subgoalsValue; this.rule = ruleValue; } /** - * Simple constructor. + * Simple constructor for a terminal proof step. * * @param goalValue the goal - * @param subgoalsValue the subgoals * @param ruleValue the rule */ - public CompositionProof(final String goalValue, final List subgoalsValue, - final CompositionRule ruleValue) { - this.goal = goalValue; - this.subgoals = subgoalsValue; - this.rule = ruleValue; + public CompositionProof(final String goalValue, final CompositionRule ruleValue) { + this(goalValue, new LinkedList(), ruleValue); } /** diff --git a/virage/src/main/resources/c_implementations/wrapper.c b/virage/src/main/resources/c_implementations/wrapper.c index 869fb71..5662b26 100644 --- a/virage/src/main/resources/c_implementations/wrapper.c +++ b/virage/src/main/resources/c_implementations/wrapper.c @@ -25,9 +25,9 @@ char** split_string(char* str) { return res; } -int find_order_index(char* candidate) { +int find_order_index(char* alternative) { for (int i = 0; i < C; i++) { - if (!strcmp(candidate, order[i])) return i; + if (!strcmp(alternative, order[i])) return i; } return C; diff --git a/virage/src/main/resources/code_file.template b/virage/src/main/resources/code_file.template index 7289df2..c753081 100644 --- a/virage/src/main/resources/code_file.template +++ b/virage/src/main/resources/code_file.template @@ -7,7 +7,7 @@ // via an additional header or via gcc option "-D DEFAULT_X="concrete implementation"", // where "concrete implementation" has to be supplied by the user. // -// "V" and "C": These defines specify the number of Voters and Candidates. For SBMC +// "V" and "C": These defines specify the number of Voters and Alternatives. For SBMC // performance, these have to be known at compile time. Default values are 3 and 3, // but they have to fit your test instances. If the numbers don't match, segmentation // faults and undefined behaviour will occur. Recompile and explicitly set the correct diff --git a/virage/src/main/resources/edu/kit/kastel/formal/beast/highlevel/javafx/BEAST.fxml b/virage/src/main/resources/edu/kit/kastel/formal/beast/highlevel/javafx/BEAST.fxml index dd22382..96ea06c 100644 --- a/virage/src/main/resources/edu/kit/kastel/formal/beast/highlevel/javafx/BEAST.fxml +++ b/virage/src/main/resources/edu/kit/kastel/formal/beast/highlevel/javafx/BEAST.fxml @@ -251,7 +251,7 @@ - + @@ -261,7 +261,7 @@ - + @@ -271,7 +271,7 @@ - + @@ -354,7 +354,7 @@ - @@ -458,9 +458,9 @@
- + - + @@ -480,8 +480,8 @@