Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

CSV Statistics Export: Ambiguous Usage of Comma #1533

Closed
wadoon opened this issue Dec 23, 2022 · 0 comments
Closed

CSV Statistics Export: Ambiguous Usage of Comma #1533

wadoon opened this issue Dec 23, 2022 · 0 comments
Labels
Command Line Interface GUI HacKeYthon Candidate Issue for HacKeYthon '24 P:LOW

Comments

@wadoon
Copy link
Member

wadoon commented Dec 23, 2022

This issue was created at git.key-project.org where the discussions are preserved.


When saving the proof statistics as CSV, a comma is used for separating columns, but also as thousands separator, as in

Total rule apps,2,965

It would be advantageous to use, e.g., semicolons instead as columns separator.

Also, the first line in

ShowProofStatistics.getCSVStatisticsMessage(proof);
File file = new File(MiscTools.toValidFileName(proof.name().toString()) + ".csv");
try (BufferedWriter writer =
        new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file)));
        ) {
    writer.write(ShowProofStatistics.getCSVStatisticsMessage(proof));
} catch (IOException e) {
    e.printStackTrace();
    assert false;
}

of class ConsoleUserInterface seems superfluous.

I git-blamed (at)mkirsten for this, at least for ConsoleUserInterface ;) Cheers!


Information:

  • created_at: 2020-04-20T07:40:51.367Z
  • updated_at: 2020-04-20T13:14:07.714Z
  • closed_at: None (closed_by: )
  • milestone:
  • user_notes_count: 3
@wadoon wadoon changed the title <placeholder> CSV Statistics Export: Ambiguous Usage of Comma Dec 24, 2022
@mi-ki mi-ki added the HacKeYthon Candidate Issue for HacKeYthon '24 label Feb 16, 2024
JonasKlamroth added a commit to JonasKlamroth/key that referenced this issue Feb 21, 2024
@JonasKlamroth JonasKlamroth mentioned this issue Feb 21, 2024
7 tasks
wadoon pushed a commit to JonasKlamroth/key that referenced this issue Feb 23, 2024
github-merge-queue bot pushed a commit that referenced this issue Feb 23, 2024
@wadoon wadoon closed this as completed Feb 24, 2024
wadoon added a commit to wadoon/key that referenced this issue Mar 10, 2024
# By Drodt (57) and others
# Via GitHub (17) and others
* origin/main: (147 commits)
  Merge main into extraxt-new-core
  fixes KeYProject#1533
  added checkbox to disable example loader directly in dialog
  address reviewer comments:
  set border + spotless + typo
  JML enabled keys indicator for the status line
  add test case for adt taclets
  Fix position info for equality expr errors
  Revert debugging code
  Spotless
  Add ADT Deconstructors
  Moved TestSMTMod to newsmt2
  spotless applied to TestSMTMod
  Added test for Modulo Translation
  Added translation from KeY mod to SMT mod. Soundness derived from translation of KeY div to SMT div
  preventing NPEs in overloaded operators
  added test cases for operator overloading
  activate the OverloadedOperatorHandler.java for LocSet datatype and repair translation
  Bump ch.qos.logback:logback-classic from 1.4.14 to 1.5.0
  Update README.md (license date and Java version)
  ...

# Conflicts:
#	key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java
#	key.core/src/main/java/de/uka/ilkd/key/settings/GeneralSettings.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLConstruct.java
#	key.ui/build.gradle
#	keyext.caching/src/test/java/de/uka/ilkd/key/proof/reference/TestReferenceSearcher.java
wadoon added a commit that referenced this issue Mar 14, 2024
# By Drodt (57) and others
# Via GitHub (26) and others
* origin/main: (158 commits)
  ColorSettings: drop old configuration file format
  Merge main into extraxt-new-core
  Bump ch.qos.logback:logback-classic from 1.5.0 to 1.5.3
  fixes #1533
  added checkbox to disable example loader directly in dialog
  address reviewer comments:
  set border + spotless + typo
  JML enabled keys indicator for the status line
  add test case for adt taclets
  Fix position info for equality expr errors
  Revert debugging code
  Spotless
  Add ADT Deconstructors
  Moved TestSMTMod to newsmt2
  spotless applied to TestSMTMod
  Added test for Modulo Translation
  Added translation from KeY mod to SMT mod. Soundness derived from translation of KeY div to SMT div
  preventing NPEs in overloaded operators
  added test cases for operator overloading
  activate the OverloadedOperatorHandler.java for LocSet datatype and repair translation
  ...

# Conflicts:
#	key.core/src/main/java/de/uka/ilkd/key/logic/op/LocationVariable.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FieldTypeToSortCondition.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticFieldCondition.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java
wadoon added a commit to wadoon/key that referenced this issue Mar 16, 2024
* main: (149 commits)
  ColorSettings: drop old configuration file format
  Merge main into extraxt-new-core
  Bump ch.qos.logback:logback-classic from 1.5.0 to 1.5.3
  fixes KeYProject#1533
  added checkbox to disable example loader directly in dialog
  address reviewer comments:
  set border + spotless + typo
  JML enabled keys indicator for the status line
  add test case for adt taclets
  Fix position info for equality expr errors
  Revert debugging code
  Spotless
  Add ADT Deconstructors
  Moved TestSMTMod to newsmt2
  spotless applied to TestSMTMod
  Added test for Modulo Translation
  Added translation from KeY mod to SMT mod. Soundness derived from translation of KeY div to SMT div
  preventing NPEs in overloaded operators
  added test cases for operator overloading
  activate the OverloadedOperatorHandler.java for LocSet datatype and repair translation
  ...

# Conflicts:
#	key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/AbstractSideProofRule.java
#	key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ModalitySideProofRule.java
#	key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java
#	key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabelManager.java
#	key.core/src/main/java/de/uka/ilkd/key/pp/AbbrevMap.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/Statistics.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/io/intermediate/MergeAppIntermediate.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/io/intermediate/MergePartnerAppIntermediate.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/io/intermediate/SMTAppIntermediate.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/io/intermediate/TacletAppIntermediate.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/ObserverToUpdateRule.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/WhileInvariantRule.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/merge/MergeRule.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/merge/procedures/MergeByIfThenElse.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java
#	key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/DefinedSymbolsHandler.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlIO.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java
#	key.core/src/main/java/de/uka/ilkd/key/util/mergerule/MergeRuleUtils.java
#	key.core/src/main/java/de/uka/ilkd/key/util/mergerule/SymbolicExecutionState.java
#	key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProveTest.java
#	key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingTestFile.java
#	key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestFile.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/mergerule/MergeProcedureCompletion.java
#	keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java
#	keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java
#	keyext.slicing/src/main/java/org/key_project/slicing/ui/ShowNodeInfoAction.java
#	keyext.slicing/src/test/java/org/key_project/slicing/DependencyGraphTest.java
wadoon added a commit that referenced this issue Mar 17, 2024
# By Drodt (57) and others
# Via GitHub (25) and others
* origin/main: (157 commits)
  ColorSettings: drop old configuration file format
  Merge main into extraxt-new-core
  Bump ch.qos.logback:logback-classic from 1.5.0 to 1.5.3
  fixes #1533
  added checkbox to disable example loader directly in dialog
  address reviewer comments:
  set border + spotless + typo
  JML enabled keys indicator for the status line
  add test case for adt taclets
  Fix position info for equality expr errors
  Revert debugging code
  Spotless
  Add ADT Deconstructors
  Moved TestSMTMod to newsmt2
  spotless applied to TestSMTMod
  Added test for Modulo Translation
  Added translation from KeY mod to SMT mod. Soundness derived from translation of KeY div to SMT div
  preventing NPEs in overloaded operators
  added test cases for operator overloading
  activate the OverloadedOperatorHandler.java for LocSet datatype and repair translation
  ...

# Conflicts:
#	key.core/src/main/java/de/uka/ilkd/key/logic/sort/AbstractSort.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/sort/Sort.java
#	key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java
#	key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DefaultBuilder.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java
#	key.core/src/test/java/de/uka/ilkd/key/parser/TestDeclParser.java
wadoon added a commit that referenced this issue Mar 17, 2024
# By Drodt (57) and others
# Via GitHub (9) and others
* main: (103 commits)
  ColorSettings: drop old configuration file format
  Merge main into extraxt-new-core
  Bump ch.qos.logback:logback-classic from 1.5.0 to 1.5.3
  fixes #1533
  added checkbox to disable example loader directly in dialog
  address reviewer comments:
  set border + spotless + typo
  JML enabled keys indicator for the status line
  add test case for adt taclets
  Fix position info for equality expr errors
  Revert debugging code
  Spotless
  Add ADT Deconstructors
  Moved TestSMTMod to newsmt2
  spotless applied to TestSMTMod
  Added test for Modulo Translation
  Added translation from KeY mod to SMT mod. Soundness derived from translation of KeY div to SMT div
  Document ncore
  Fix merge import errors
  Fix merge errors
  ...

# Conflicts:
#	key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ClassAxiomAndInvariantProofReferencesAnalyst.java
#	key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionAuxiliaryContract.java
#	key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleInvariantTranslator.java
#	key.core/build.gradle
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/BlockExecutionPO.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowContractPO.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/LoopInvExecutionPO.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/SymbolicExecutionPO.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/TwoStateMethodPredicateSnippet.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/BlockInfFlowUnfoldTacletBuilder.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/InfFlowBlockContractTacletBuilder.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/InfFlowLoopInvariantTacletBuilder.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/LoopInfFlowUnfoldTacletBuilder.java
#	key.core/src/main/java/de/uka/ilkd/key/java/JavaInfo.java
#	key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeY.java
#	key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java
#	key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYTypeConverter.java
#	key.core/src/main/java/de/uka/ilkd/key/java/Services.java
#	key.core/src/main/java/de/uka/ilkd/key/java/TypeConverter.java
#	key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/KeYJavaType.java
#	key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/Literal.java
#	key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/DLEmbeddedExpression.java
#	key.core/src/main/java/de/uka/ilkd/key/java/expression/literal/EmptyMapLiteral.java
#	key.core/src/main/java/de/uka/ilkd/key/java/expression/literal/FreeLiteral.java
#	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SchemaJavaProgramFactory.java
#	key.core/src/main/java/de/uka/ilkd/key/ldt/BooleanLDT.java
#	key.core/src/main/java/de/uka/ilkd/key/ldt/CharListLDT.java
#	key.core/src/main/java/de/uka/ilkd/key/ldt/DoubleLDT.java
#	key.core/src/main/java/de/uka/ilkd/key/ldt/FloatLDT.java
#	key.core/src/main/java/de/uka/ilkd/key/ldt/FreeLDT.java
#	key.core/src/main/java/de/uka/ilkd/key/ldt/HeapLDT.java
#	key.core/src/main/java/de/uka/ilkd/key/ldt/IntegerLDT.java
#	key.core/src/main/java/de/uka/ilkd/key/ldt/LDT.java
#	key.core/src/main/java/de/uka/ilkd/key/ldt/LocSetLDT.java
#	key.core/src/main/java/de/uka/ilkd/key/ldt/MapLDT.java
#	key.core/src/main/java/de/uka/ilkd/key/ldt/PermissionLDT.java
#	key.core/src/main/java/de/uka/ilkd/key/ldt/RealLDT.java
#	key.core/src/main/java/de/uka/ilkd/key/ldt/SeqLDT.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/op/IProgramVariable.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/op/LocationVariable.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramConstant.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramVariable.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/sort/ArraySort.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/AbstractBlastingMacro.java
#	key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java
#	key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DefaultBuilder.java
#	key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java
#	key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java
#	key.core/src/main/java/de/uka/ilkd/key/pp/SelectPrinter.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/NodeInfo.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/TacletIndex.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractOperationPO.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/init/DependencyContractPO.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalBlockContractPO.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalLoopContractPO.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/AbstractAuxiliaryContractRule.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBlockContractRule.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopContractRule.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/ObserverToUpdateRule.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/QueryExpand.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/inst/SVInstantiations.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/merge/MergeRuleBuiltInRuleApp.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ArrayPostDecl.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ConstantValue.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ConstructorCall.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/EnhancedForElimination.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/EnumConstantValue.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/MethodCall.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/MultipleVarDecl.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ObserverEqualityMetaConstruct.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/SpecialConstructorCall.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java
#	key.core/src/main/java/de/uka/ilkd/key/smt/SMTObjTranslator.java
#	key.core/src/main/java/de/uka/ilkd/key/smt/hierarchy/TypeHierarchy.java
#	key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/FieldConstantHandler.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/ClassAxiomImpl.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/ClassWellDefinedness.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/ContractAxiom.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/MethodWellDefinedness.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/RepresentsAxiom.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/WellDefinednessCheck.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLExpression.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLMethodResolver.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLParameters.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLTranslationException.java
#	key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/TacletProofObligationInput.java
#	key.core/src/test/java/de/uka/ilkd/key/java/visitor/TestDeclarationProgramVariableCollector.java
#	key.core/src/test/java/de/uka/ilkd/key/logic/TestTerm.java
#	key.core/src/test/java/de/uka/ilkd/key/logic/TestTermFactory.java
#	key.core/src/test/java/de/uka/ilkd/key/rule/TacletForTests.java
#	key.core/src/test/java/de/uka/ilkd/key/speclang/njml/ClasslevelTranslatorTest.java
#	key.core/src/test/java/de/uka/ilkd/key/speclang/njml/ExpressionTranslatorTest.java
#	key.ui/build.gradle
#	key.ui/src/main/java/de/uka/ilkd/key/gui/ProofManagementDialog.java
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Command Line Interface GUI HacKeYthon Candidate Issue for HacKeYthon '24 P:LOW
Projects
Status: In Progress
Development

No branches or pull requests

2 participants