From 80974e045e057b6adc0306fa39108b0a2dd8f155 Mon Sep 17 00:00:00 2001
From: penguinn <michellewerth@hotmail.com>
Date: Thu, 17 Jan 2019 14:52:14 +0100
Subject: [PATCH] Rearrange handbook files and merge developer handbook and
user manual
---
build.gradle | 2 +-
config.yaml | 13 +-
...1_The_ProB_Animator_and_Model_Checker.adoc | 2 +
...00_General.adoc => 00_section_header.adoc} | 2 +
.../user/10_General/01_Installation.adoc | 13 +-
.../02_Windows_Installation_Instructions.adoc | 17 +-
.../chapter/user/10_General/10_Animation.adoc | 17 +-
.../10_General}/Building_ProB_on_Windows.adoc | 2 +-
.../Colours_of_enabled_operations.adoc | 3 +-
.../Controlling_ProB_Preferences.adoc | 9 +-
.../user/10_General/Current_Limitations.adoc | 5 +-
.../user/10_General/Deferred_Sets.adoc | 7 +-
.../user/10_General/Editors_for_ProB.adoc | 17 +-
.../user/10_General/GeneralPresentation.adoc | 7 +-
.../10_General}/Getting_Involved.adoc | 2 +-
.../10_General/ProB_Logic_Calculator_old.adoc | 11 +-
.../10_General}/ZZ_section_footer.adoc | 1 +
..._BLanguage.adoc => 00_section_header.adoc} | 2 +
.../11_BLanguage/01_Summary_of_B_Syntax.adoc | 45 +--
.../chapter/user/11_BLanguage/02_Types.adoc | 11 +-
.../11_BLanguage/10_External_Functions.adoc | 7 +-
.../11_Recursively_Defined_Functions.adoc | 11 +-
.../user/11_BLanguage/20_Tips:_B_Idioms.adoc | 34 +-
.../21_Tips:_Writing_Models_for_ProB.adoc | 12 +-
.../11_BLanguage/WD/00_section_header.adoc | 4 +
.../WD/01_Well-Definedness_Checking.adoc | 3 +-
.../11_BLanguage/WD}/ZZ_section_footer.adoc | 1 +
.../11_BLanguage}/ZZ_section_footer.adoc | 1 +
.../user/20_Validation/00_section_header.adoc | 4 +
.../20_Validation/CBC/00_section_header.adoc | 19 +
.../CBC/01_Constraint_Based_Checking.adoc | 23 +-
.../CBC/10_Bounded_Model_Checking.adoc | 3 +-
.../CBC/20_Symbolic_Model_Checking.adoc | 9 +-
.../20_Validation/CBC/ZZ_section_footer.adoc | 2 +
.../20_Validation/MC/00_section_header.adoc | 4 +
.../MC/01_Consistency_Checking.adoc | 25 +-
.../MC/10_Distributed_Model_Checking.adoc | 11 +-
.../chapter/user/20_Validation/MC/11_DMC.adoc | 14 +-
.../user/20_Validation/MC/12_ParB.adoc | 9 +-
.../MC/20_LTL_Model_Checking.adoc | 21 +-
.../MC/30_Symmetry_Reduction.adoc | 9 +-
.../chapter/user/20_Validation/MC/40_LTSmin | 4 +-
.../20_Validation/MC/ZZ_section_footer.adoc | 2 +
...hods.adoc => ProB_Validation_Methods.adoc} | 1 +
.../20_Validation/Refinement_Checking.adoc | 7 +-
.../user/20_Validation/ZZ_section_footer.adoc | 2 +
...00_Testing.adoc => 00_section_header.adoc} | 2 +
.../10_State_Space_Coverage_Analyses.adoc | 5 +-
.../21_Testing/11_Test_Case_Generation.adoc | 25 +-
.../20_Tutorial_Model-Based_Testing.adoc | 7 +-
.../user/21_Testing/ZZ_section_footer.adoc | 2 +
...ualisation.adoc => 00_section_header.adoc} | 2 +
.../22_Visualisation/10_Graphical_Viewer.adoc | 6 +-
.../20_State_Space_Visualization.adoc | 13 +-
...21_State_space_visualization_examples.adoc | 19 +-
.../22_Visualisation/30_Eval_Console.adoc | 3 +-
.../22_Visualisation/31_Evaluation_View.adoc | 9 +-
.../40_Graphical_Visualization.adoc | 16 +-
.../22_Visualisation/ZZ_section_footer.adoc | 2 +
...ommandLine.adoc => 00_section_header.adoc} | 2 +
.../user/25_CommandLine/01_ProB_Cli.adoc | 2 +-
...sing_the_Command-Line_Version_of_ProB.adoc | 367 +++++++++---------
.../25_CommandLine/ZZ_section_footer.adoc | 2 +
.../30_OtherLanguages/00_section_header.adoc | 4 +
...languages.adoc => 01_Other_languages.adoc} | 7 +-
.../chapter/user/30_OtherLanguages/Alloy.adoc | 29 +-
.../CSP}/00_section_header.adoc | 4 +-
.../user/30_OtherLanguages/CSP/01_CSP-M.adoc | 10 +-
.../CSP/02_CSP-M_Syntax.adoc | 16 +-
.../CSP/03_Checking_CSP_Assertions.adoc | 12 +-
.../CSP/ZZ_section_footer.adoc | 2 +
.../EventB/00_section_header.adoc | 4 +
.../30_OtherLanguages/EventB/01_Event-B.adoc | 15 +-
.../EventB/02_Event-B_Theories.adoc | 9 +-
.../EventB/ProB_for_Event-B.adoc | 3 +-
.../EventB/ProB_for_Rodin.adoc | 15 +-
.../EventB/ZZ_section_footer.adoc | 2 +
.../chapter/user/30_OtherLanguages/ProZ.adoc | 45 +--
.../chapter/user/30_OtherLanguages/TLA.adoc | 17 +-
.../30_OtherLanguages/ZZ_section_footer.adoc | 2 +
...d_Features.adoc => 00_section_header.adoc} | 2 +
.../00_section_header.adoc | 4 +
.../01_Bash_Completion.adoc | 7 +-
.../02_Common_Subexpression_Elimination.adoc | 13 +-
.../01_Feature_Description/03_PROBPATH.adoc | 3 +-
.../01_Feature_Description/04_TLC.adoc | 19 +-
.../ZZ_section_footer.adoc | 2 +
.../02_Using_ProB/00_section_header.adoc | 4 +
...erating_Documents_with_ProB_and_Latex.adoc | 9 +-
.../Using_ProB_with_Atelier_B.adoc | 11 +-
.../02_Using_ProB/Using_ProB_with_KODKOD.adoc | 15 +-
.../02_Using_ProB/Using_ProB_with_Z3.adoc | 11 +-
.../02_Using_ProB/ZZ_section_footer.adoc | 2 +
.../ZZ_section_footer.adoc | 2 +
.../{00_ProB2.adoc => 00_section_header.adoc} | 2 +
.../50_ProB2/01_ProB_2.0_Development.adoc | 13 +-
...odin_and_a_HTML_Visualization_Example.adoc | 13 +-
.../user/50_ProB2/Prob2-advance-release.adoc | 4 +-
.../user/50_ProB2/ZZ_section_footer.adoc | 2 +
.../user/51_JavaFX/00_section_header.adoc | 4 +
.../01_ProB2_JavaFX_UI.adoc | 22 +-
.../JavaFX => 51_JavaFX}/11_History_View.adoc | 3 +-
.../JavaFX => 51_JavaFX}/12_Project_View.adoc | 13 +-
.../13_Verification_View.adoc | 9 +-
.../14_Statistics_View.adoc | 3 +-
.../user/51_JavaFX/ZZ_section_footer.adoc | 2 +
.../52_Prolog}/00_section_header.adoc | 2 +
.../Organization_of_ProB_Sources.adoc | 1 +
.../ProB's_Prolog_Datastructures.adoc | 1 +
.../52_Prolog}/Prolog_Coding_Guidelines.adoc | 5 +-
.../52_Prolog}/Running_ProB_from_source.adoc | 1 +
.../52_Prolog}/Why_Prolog.adoc | 1 -
.../user/52_Prolog/ZZ_section_footer.adoc | 2 +
.../chapter/user/55_JavaAPI/00_JavaAPI.adoc | 2 -
.../user/60_JavaAPI/00_section_header.adoc | 4 +
.../01_ProB_Java_API.adoc | 9 +-
.../02_ProB_Java_API_Tutorial.adoc | 39 +-
...atic_Abstractions_in_the_ProB_2.0_API.adoc | 15 +-
...nd_Developer_Workshop_2013_-_Tutorial.adoc | 21 +-
.../user/60_JavaAPI/ZZ_section_footer.adoc | 2 +
.../65_Java_2-0_API}/00_section_header.adoc | 1 +
.../65_Java_2-0_API}/01_introduction.adoc | 1 +
.../65_Java_2-0_API}/02_architecture.adoc | 2 +
.../65_Java_2-0_API}/03_installation.adoc | 2 +
.../65_Java_2-0_API}/04_lowlevelapi.adoc | 2 +
.../65_Java_2-0_API}/05_probcore.adoc | 2 +
.../65_Java_2-0_API}/06_animation.adoc | 2 +
.../65_Java_2-0_API}/07_evaluation.adoc | 2 +
.../65_Java_2-0_API}/08_cosimulation.adoc | 2 +
.../09_dependencyinjection.adoc | 2 +
.../65_Java_2-0_API/ZZ_section_footer.adoc | 2 +
.../user/70_TclTk/00_section_header.adoc | 4 +
.../70_TclTk}/Tk_Architecture.adoc | 0
.../user/70_TclTk/ZZ_section_footer.adoc | 2 +
.../user/YZ_Tutorials/00_section_header.adoc | 4 +
.../Tutorial_Animation_Tips.adoc | 17 +-
.../Tutorial_CSP_First_Step.adoc} | 15 +-
.../Tutorial_Co-Simulation.adoc | 5 +-
.../Tutorial_Complete_Model_Checking.adoc | 13 +-
...ll-Definedness_and_Transition_Errors.adoc} | 5 +-
.../Tutorial_Directed_Model_Checking.adoc | 17 +-
.../Tutorial_Disprover.adoc | 13 +-
.../Tutorial_Enabling_Analysis.adoc} | 11 +-
.../Tutorial_First_Model_Checking.adoc | 9 +-
.../Tutorial_First_Step.adoc | 11 +-
.../Tutorial_LTL_Counter-example_View.adoc | 13 +-
...utorial_Model_Checking_Proof_and_CBC.adoc} | 9 +-
...Tutorial_Modeling_Infinite_Datatypes.adoc} | 3 +-
.../Tutorial_Rodin_Exporting.adoc | 11 +-
.../Tutorial_Rodin_First_Step.adoc | 7 +-
.../Tutorial_Rodin_Parameters.adoc | 11 +-
.../Tutorial_Setup_Phases.adoc | 9 +-
.../Tutorial_Symbolic_Constants.adoc | 9 +-
.../Tutorial_Troubleshooting_the_Setup.adoc | 7 +-
...nderstanding_ProB's_Constraint_Solver.adoc | 9 +-
...tanding_the_Complexity_of_B_Animation.adoc | 7 +-
.../Tutorial_Unit_Plugin.adoc | 11 +-
.../Tutorial_Unit_Plugin_With_Rodin.adoc | 11 +-
.../Tutorial_Various_Optimizations.adoc | 9 +-
.../user/YZ_Tutorials/ZZ_section_footer.adoc | 3 +
.../00_section_header.adoc} | 2 +
.../{70_Appendix => ZZ_Appendix}/01_Team.adoc | 2 +-
.../{70_Appendix => ZZ_Appendix}/02_FAQ.adoc | 32 +-
.../03_Download.adoc | 2 +-
.../04_DownloadPriorVersions.adoc | 2 +-
.../05_Links.adoc | 18 +-
.../06_ProB_Release_History.adoc | 2 +-
.../{70_Appendix => ZZ_Appendix}/10_Bugs.adoc | 2 +-
.../11_Troubleshooting.adoc | 2 +-
.../20_ProBLicence.adoc | 2 +-
.../ZZ_Appendix}/A_literature.adoc | 1 +
.../ZZ_Appendix}/B_preferences.adoc | 1 +
.../user/ZZ_Appendix/ZZ_section_footer.adoc | 3 +
173 files changed, 982 insertions(+), 773 deletions(-)
rename src/docs/chapter/user/10_General/{00_General.adoc => 00_section_header.adoc} (55%)
rename src/docs/chapter/{developer => user/10_General}/Building_ProB_on_Windows.adoc (100%)
rename src/docs/chapter/{developer => user/10_General}/Getting_Involved.adoc (100%)
rename src/docs/chapter/{developer/30_tcltk => user/10_General}/ZZ_section_footer.adoc (94%)
rename src/docs/chapter/user/11_BLanguage/{00_BLanguage.adoc => 00_section_header.adoc} (60%)
create mode 100644 src/docs/chapter/user/11_BLanguage/WD/00_section_header.adoc
rename src/docs/chapter/{developer/10_java_api => user/11_BLanguage/WD}/ZZ_section_footer.adoc (94%)
rename src/docs/chapter/{developer/20_prolog => user/11_BLanguage}/ZZ_section_footer.adoc (94%)
create mode 100644 src/docs/chapter/user/20_Validation/00_section_header.adoc
create mode 100644 src/docs/chapter/user/20_Validation/CBC/00_section_header.adoc
create mode 100644 src/docs/chapter/user/20_Validation/CBC/ZZ_section_footer.adoc
create mode 100644 src/docs/chapter/user/20_Validation/MC/00_section_header.adoc
create mode 100644 src/docs/chapter/user/20_Validation/MC/ZZ_section_footer.adoc
rename src/docs/chapter/user/20_Validation/{00_ProB_Validation_Methods.adoc => ProB_Validation_Methods.adoc} (99%)
create mode 100644 src/docs/chapter/user/20_Validation/ZZ_section_footer.adoc
rename src/docs/chapter/user/21_Testing/{00_Testing.adoc => 00_section_header.adoc} (55%)
create mode 100644 src/docs/chapter/user/21_Testing/ZZ_section_footer.adoc
rename src/docs/chapter/user/22_Visualisation/{00_Visualisation.adoc => 00_section_header.adoc} (65%)
create mode 100644 src/docs/chapter/user/22_Visualisation/ZZ_section_footer.adoc
rename src/docs/chapter/user/25_CommandLine/{00_CommandLine.adoc => 00_section_header.adoc} (64%)
create mode 100644 src/docs/chapter/user/25_CommandLine/ZZ_section_footer.adoc
create mode 100644 src/docs/chapter/user/30_OtherLanguages/00_section_header.adoc
rename src/docs/chapter/user/30_OtherLanguages/{00_Other_languages.adoc => 01_Other_languages.adoc} (98%)
rename src/docs/chapter/{developer/30_tcltk => user/30_OtherLanguages/CSP}/00_section_header.adoc (53%)
create mode 100644 src/docs/chapter/user/30_OtherLanguages/CSP/ZZ_section_footer.adoc
create mode 100644 src/docs/chapter/user/30_OtherLanguages/EventB/00_section_header.adoc
create mode 100644 src/docs/chapter/user/30_OtherLanguages/EventB/ZZ_section_footer.adoc
create mode 100644 src/docs/chapter/user/30_OtherLanguages/ZZ_section_footer.adoc
rename src/docs/chapter/user/40_AdvancedFeatures/{00_Advanced_Features.adoc => 00_section_header.adoc} (92%)
create mode 100644 src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/00_section_header.adoc
create mode 100644 src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/ZZ_section_footer.adoc
create mode 100644 src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/00_section_header.adoc
create mode 100644 src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/ZZ_section_footer.adoc
create mode 100644 src/docs/chapter/user/40_AdvancedFeatures/ZZ_section_footer.adoc
rename src/docs/chapter/user/50_ProB2/{00_ProB2.adoc => 00_section_header.adoc} (56%)
create mode 100644 src/docs/chapter/user/50_ProB2/ZZ_section_footer.adoc
create mode 100644 src/docs/chapter/user/51_JavaFX/00_section_header.adoc
rename src/docs/chapter/user/{50_ProB2/JavaFX => 51_JavaFX}/01_ProB2_JavaFX_UI.adoc (93%)
rename src/docs/chapter/user/{50_ProB2/JavaFX => 51_JavaFX}/11_History_View.adoc (97%)
rename src/docs/chapter/user/{50_ProB2/JavaFX => 51_JavaFX}/12_Project_View.adoc (95%)
rename src/docs/chapter/user/{50_ProB2/JavaFX => 51_JavaFX}/13_Verification_View.adoc (92%)
rename src/docs/chapter/user/{50_ProB2/JavaFX => 51_JavaFX}/14_Statistics_View.adoc (93%)
create mode 100644 src/docs/chapter/user/51_JavaFX/ZZ_section_footer.adoc
rename src/docs/chapter/{developer/20_prolog => user/52_Prolog}/00_section_header.adoc (61%)
rename src/docs/chapter/{developer/20_prolog => user/52_Prolog}/Organization_of_ProB_Sources.adoc (98%)
rename src/docs/chapter/{developer/20_prolog => user/52_Prolog}/ProB's_Prolog_Datastructures.adoc (99%)
rename src/docs/chapter/{developer/20_prolog => user/52_Prolog}/Prolog_Coding_Guidelines.adoc (98%)
rename src/docs/chapter/{developer/20_prolog => user/52_Prolog}/Running_ProB_from_source.adoc (99%)
rename src/docs/chapter/{developer/20_prolog => user/52_Prolog}/Why_Prolog.adoc (99%)
create mode 100644 src/docs/chapter/user/52_Prolog/ZZ_section_footer.adoc
delete mode 100644 src/docs/chapter/user/55_JavaAPI/00_JavaAPI.adoc
create mode 100644 src/docs/chapter/user/60_JavaAPI/00_section_header.adoc
rename src/docs/chapter/user/{55_JavaAPI => 60_JavaAPI}/01_ProB_Java_API.adoc (94%)
rename src/docs/chapter/user/{55_JavaAPI => 60_JavaAPI}/02_ProB_Java_API_Tutorial.adoc (94%)
rename src/docs/chapter/user/{55_JavaAPI => 60_JavaAPI}/10_Programmatic_Abstractions_in_the_ProB_2.0_API.adoc (96%)
rename src/docs/chapter/user/{55_JavaAPI => 60_JavaAPI}/20_Rodin_User_and_Developer_Workshop_2013_-_Tutorial.adoc (98%)
create mode 100644 src/docs/chapter/user/60_JavaAPI/ZZ_section_footer.adoc
rename src/docs/chapter/{developer/10_java_api => user/65_Java_2-0_API}/00_section_header.adoc (98%)
rename src/docs/chapter/{developer/10_java_api => user/65_Java_2-0_API}/01_introduction.adoc (99%)
rename src/docs/chapter/{developer/10_java_api => user/65_Java_2-0_API}/02_architecture.adoc (98%)
rename src/docs/chapter/{developer/10_java_api => user/65_Java_2-0_API}/03_installation.adoc (96%)
rename src/docs/chapter/{developer/10_java_api => user/65_Java_2-0_API}/04_lowlevelapi.adoc (99%)
rename src/docs/chapter/{developer/10_java_api => user/65_Java_2-0_API}/05_probcore.adoc (99%)
rename src/docs/chapter/{developer/10_java_api => user/65_Java_2-0_API}/06_animation.adoc (99%)
rename src/docs/chapter/{developer/10_java_api => user/65_Java_2-0_API}/07_evaluation.adoc (99%)
rename src/docs/chapter/{developer/10_java_api => user/65_Java_2-0_API}/08_cosimulation.adoc (97%)
rename src/docs/chapter/{developer/10_java_api => user/65_Java_2-0_API}/09_dependencyinjection.adoc (99%)
create mode 100644 src/docs/chapter/user/65_Java_2-0_API/ZZ_section_footer.adoc
create mode 100644 src/docs/chapter/user/70_TclTk/00_section_header.adoc
rename src/docs/chapter/{developer/30_tcltk => user/70_TclTk}/Tk_Architecture.adoc (100%)
create mode 100644 src/docs/chapter/user/70_TclTk/ZZ_section_footer.adoc
create mode 100644 src/docs/chapter/user/YZ_Tutorials/00_section_header.adoc
rename src/docs/chapter/user/{10_General => YZ_Tutorials}/Tutorial_Animation_Tips.adoc (93%)
rename src/docs/chapter/user/{30_OtherLanguages/CSP/04_Tutorial_CSP_First_Step.adoc => YZ_Tutorials/Tutorial_CSP_First_Step.adoc} (96%)
rename src/docs/chapter/user/{40_AdvancedFeatures/10_Tutorials => YZ_Tutorials}/Tutorial_Co-Simulation.adoc (96%)
rename src/docs/chapter/user/{20_Validation/MC => YZ_Tutorials}/Tutorial_Complete_Model_Checking.adoc (97%)
rename src/docs/chapter/user/{11_BLanguage/WD/10_Tutorial_Debugging_Well-Definedness_and_Transition_Errors.adoc => YZ_Tutorials/Tutorial_Debugging_Well-Definedness_and_Transition_Errors.adoc} (96%)
rename src/docs/chapter/user/{20_Validation/MC => YZ_Tutorials}/Tutorial_Directed_Model_Checking.adoc (98%)
rename src/docs/chapter/user/{40_AdvancedFeatures/10_Tutorials => YZ_Tutorials}/Tutorial_Disprover.adoc (95%)
rename src/docs/chapter/user/{20_Validation/CBC/30_Tutorial_Enabling_Analysis.adoc => YZ_Tutorials/Tutorial_Enabling_Analysis.adoc} (99%)
rename src/docs/chapter/user/{20_Validation/MC => YZ_Tutorials}/Tutorial_First_Model_Checking.adoc (97%)
rename src/docs/chapter/user/{10_General => YZ_Tutorials}/Tutorial_First_Step.adoc (97%)
rename src/docs/chapter/user/{20_Validation/MC => YZ_Tutorials}/Tutorial_LTL_Counter-example_View.adoc (98%)
rename src/docs/chapter/user/{20_Validation/CBC/31_Tutorial_Model_Checking,_Proof_and_CBC.adoc => YZ_Tutorials/Tutorial_Model_Checking_Proof_and_CBC.adoc} (97%)
rename src/docs/chapter/user/{11_BLanguage/30_Tutorial_Modeling_Infinite_Datatypes.adoc => YZ_Tutorials/Tutorial_Modeling_Infinite_Datatypes.adoc} (98%)
rename src/docs/chapter/user/{30_OtherLanguages/EventB => YZ_Tutorials}/Tutorial_Rodin_Exporting.adoc (94%)
rename src/docs/chapter/user/{30_OtherLanguages/EventB => YZ_Tutorials}/Tutorial_Rodin_First_Step.adoc (97%)
rename src/docs/chapter/user/{30_OtherLanguages/EventB => YZ_Tutorials}/Tutorial_Rodin_Parameters.adoc (94%)
rename src/docs/chapter/user/{10_General => YZ_Tutorials}/Tutorial_Setup_Phases.adoc (98%)
rename src/docs/chapter/user/{40_AdvancedFeatures/10_Tutorials => YZ_Tutorials}/Tutorial_Symbolic_Constants.adoc (91%)
rename src/docs/chapter/user/{10_General => YZ_Tutorials}/Tutorial_Troubleshooting_the_Setup.adoc (98%)
rename src/docs/chapter/user/{10_General => YZ_Tutorials}/Tutorial_Understanding_ProB's_Constraint_Solver.adoc (98%)
rename src/docs/chapter/user/{10_General => YZ_Tutorials}/Tutorial_Understanding_the_Complexity_of_B_Animation.adoc (98%)
rename src/docs/chapter/user/{40_AdvancedFeatures/10_Tutorials => YZ_Tutorials}/Tutorial_Unit_Plugin.adoc (95%)
rename src/docs/chapter/user/{40_AdvancedFeatures/10_Tutorials => YZ_Tutorials}/Tutorial_Unit_Plugin_With_Rodin.adoc (92%)
rename src/docs/chapter/user/{20_Validation/MC => YZ_Tutorials}/Tutorial_Various_Optimizations.adoc (99%)
create mode 100644 src/docs/chapter/user/YZ_Tutorials/ZZ_section_footer.adoc
rename src/docs/chapter/user/{70_Appendix/00_Appendix.adoc => ZZ_Appendix/00_section_header.adoc} (57%)
rename src/docs/chapter/user/{70_Appendix => ZZ_Appendix}/01_Team.adoc (99%)
rename src/docs/chapter/user/{70_Appendix => ZZ_Appendix}/02_FAQ.adoc (91%)
rename src/docs/chapter/user/{70_Appendix => ZZ_Appendix}/03_Download.adoc (91%)
rename src/docs/chapter/user/{70_Appendix => ZZ_Appendix}/04_DownloadPriorVersions.adoc (87%)
rename src/docs/chapter/user/{70_Appendix => ZZ_Appendix}/05_Links.adoc (98%)
rename src/docs/chapter/user/{70_Appendix => ZZ_Appendix}/06_ProB_Release_History.adoc (99%)
rename src/docs/chapter/user/{70_Appendix => ZZ_Appendix}/10_Bugs.adoc (97%)
rename src/docs/chapter/user/{70_Appendix => ZZ_Appendix}/11_Troubleshooting.adoc (98%)
rename src/docs/chapter/user/{70_Appendix => ZZ_Appendix}/20_ProBLicence.adoc (98%)
rename src/docs/chapter/{appendix => user/ZZ_Appendix}/A_literature.adoc (97%)
rename src/docs/chapter/{appendix => user/ZZ_Appendix}/B_preferences.adoc (99%)
create mode 100644 src/docs/chapter/user/ZZ_Appendix/ZZ_section_footer.adoc
diff --git a/build.gradle b/build.gradle
index 0a6f688..0003d34 100644
--- a/build.gradle
+++ b/build.gradle
@@ -85,7 +85,7 @@ asciidoctor {
options doctype: 'book'
- backends = ['html5', 'pdf']
+ backends = ['html5']
attributes = [
'source-highlighter': 'coderay',
diff --git a/config.yaml b/config.yaml
index 533850d..d0acdd8 100644
--- a/config.yaml
+++ b/config.yaml
@@ -1,19 +1,10 @@
---
-file: prob_developer.adoc
-title: ProB Developer Handbook
+file: prob_handbook.adoc
+title: ProB Handbook
authors:
- Jens Bendisposto
- Joy Clark
- Michael Leuschel
-content:
- - developer
- - appendix
----
-file: prob_user_manual.adoc
-title: ProB User Manual
-authors:
- - Jens Bendisposto
- - Michael Leuschel
content:
- user
- model_examples
diff --git a/src/docs/chapter/user/01_The_ProB_Animator_and_Model_Checker.adoc b/src/docs/chapter/user/01_The_ProB_Animator_and_Model_Checker.adoc
index 60a7985..3cc978b 100644
--- a/src/docs/chapter/user/01_The_ProB_Animator_and_Model_Checker.adoc
+++ b/src/docs/chapter/user/01_The_ProB_Animator_and_Model_Checker.adoc
@@ -1,4 +1,6 @@
+
[[the-prob-animator-and-modelchecker]]
+= The ProB Animator and Modelchecker
[width="100%",cols="60%,40%",]
|=======================================================================
diff --git a/src/docs/chapter/user/10_General/00_General.adoc b/src/docs/chapter/user/10_General/00_section_header.adoc
similarity index 55%
rename from src/docs/chapter/user/10_General/00_General.adoc
rename to src/docs/chapter/user/10_General/00_section_header.adoc
index 2778c83..de736a0 100644
--- a/src/docs/chapter/user/10_General/00_General.adoc
+++ b/src/docs/chapter/user/10_General/00_section_header.adoc
@@ -1,2 +1,4 @@
+
[[general]]
= General
+:leveloffset: +1
diff --git a/src/docs/chapter/user/10_General/01_Installation.adoc b/src/docs/chapter/user/10_General/01_Installation.adoc
index ee5c34e..c050d8c 100644
--- a/src/docs/chapter/user/10_General/01_Installation.adoc
+++ b/src/docs/chapter/user/10_General/01_Installation.adoc
@@ -1,8 +1,9 @@
+
[[installation]]
-== Installation
+= Installation
[[what-are-the-available-versions]]
-=== What are the available versions?
+== What are the available versions?
* The standalone Tcl/Tk Version of ProB (ProB Tcl/Tk)
* The standalone command-line version of ProB
@@ -31,7 +32,7 @@ We are also developing a new Java-based API called
command-line version and <<using-the-command-line-version-of-prob, here>> is how to use it.
[[which-version-should-i-use]]
-=== Which version should I use?
+== Which version should I use?
The standalone version Tcl/Tk of ProB contains a richer set of features
than the Rodin version and also works on other formalisms than Event-B
@@ -43,7 +44,7 @@ ProB. Use the probcli version if you want to write batch scripts or
prefer working from the command-line.
[[installation-instruction-for-prob-standalone]]
-=== Installation Instruction for ProB (Standalone)
+== Installation Instruction for ProB (Standalone)
NOTE: We have specific <<windows-installation-instructions, Windows installation instructions>>.
These here are the generic instructions.
@@ -92,7 +93,7 @@ animate them. Have a look at the supplied Machines in the examples
directory. Have fun! Please report bugs!
[[checklisttroubleshooting]]
-==== Checklist/Troubleshooting
+=== Checklist/Troubleshooting
* Java: be sure to have Java 7 or newer installed. Otherwise you will
not be able to parse your own classical B machines as our parser is
@@ -115,6 +116,6 @@ dot viewer. See more information about the
<<graphical-viewer,Graphical Viewer here>>.
[[installation-instruction-for-prob-rodin-plugin]]
-=== Installation Instruction for ProB (Rodin Plugin)
+== Installation Instruction for ProB (Rodin Plugin)
<<tutorial-rodin-first-step,This>> tutorial shows how to properly install ProB for Rodin.
diff --git a/src/docs/chapter/user/10_General/02_Windows_Installation_Instructions.adoc b/src/docs/chapter/user/10_General/02_Windows_Installation_Instructions.adoc
index 8c9d7b8..bd38149 100644
--- a/src/docs/chapter/user/10_General/02_Windows_Installation_Instructions.adoc
+++ b/src/docs/chapter/user/10_General/02_Windows_Installation_Instructions.adoc
@@ -1,8 +1,9 @@
+
[[windows-specific-download-instructions]]
-== Windows Specific Download Instructions
+= Windows Specific Download Instructions
[[go-to-the-prob-downloads-site]]
-=== Go to the ProB Downloads site
+== Go to the ProB Downloads site
* Go to the page
https://www3.hhu.de/stups/prob/index.php/Download[Download],
@@ -11,7 +12,7 @@ this should look as follows:
image::ProBWindowsDownload.png[]
[[install-tcltk-8.5]]
-=== Install Tcl/Tk 8.5
+== Install Tcl/Tk 8.5
If Tcl/Tk 8.5 is already installed you can skip this step.
@@ -27,7 +28,7 @@ ProB.
image::TkWindowsDownload.png[]
[[install-java]]
-=== Install Java
+== Install Java
If Java 7 or newer is already installed you can skip this step.
@@ -36,7 +37,7 @@ newer)] link provided in the `Dependencies` column and the `Windows` row above
* Follow the installation instructions
[[download-the-prob-for-windows-zipfile]]
-=== Download the ProB for Windows Zipfile
+== Download the ProB for Windows Zipfile
* Click on the https://www3.hhu.de/stups/downloads/[Zipfile
(with probcli)] link in the `Downloads` column and `Windows` row
@@ -51,20 +52,20 @@ The subfolder called `Microsoft.VC80.CRT` contains the DLLs for the
Microsoft C runtime.
[[optionally-download-graphviz]]
-=== Optionally Download GraphViz
+== Optionally Download GraphViz
* Install the `dot` program and `dotty viewer` from
http://www.graphviz.org/ or http://www.research.att.com/sw/tools/graphviz/[AT&T's Graphviz package]
[[start-prob]]
-=== Start ProB
+== Start ProB
* Start ProB by double-clicking on the ProBWin icon above
* Try to open some of the examples provided in the Examples folder shown above
* Contact us if you have problems
[[checklist-troubleshooting]]
-=== Checklist/Troubleshooting
+== Checklist/Troubleshooting
* Java: be sure to have Java 1.7 or newer installed. Otherwise you will
not be able to parse your own classical B machines as our parser is
diff --git a/src/docs/chapter/user/10_General/10_Animation.adoc b/src/docs/chapter/user/10_General/10_Animation.adoc
index e89d8f0..7e58319 100644
--- a/src/docs/chapter/user/10_General/10_Animation.adoc
+++ b/src/docs/chapter/user/10_General/10_Animation.adoc
@@ -1,5 +1,6 @@
+
[[animation]]
-== Animation
+= Animation
The animation facilities of ProB allow users to gain confidence in their
specifications. These features try to be as user-friendly as possible
@@ -8,7 +9,7 @@ operation arguments or choice variables, and he uses the mouse to
operate the animation).
[[basic-animation]]
-=== Basic Animation
+== Basic Animation
When the B specification is opened, the syntax and type checker analyses
it and, if a syntax or type error is detected, it is then reported,
@@ -21,7 +22,7 @@ performed in the Enabled Operations pane. These operations can be of two
types described below.
[[operations-from-the-b-machine]]
-==== Operations from the B Machine
+=== Operations from the B Machine
These operations are the ones whose preconditions and guards are
satisfiable in the current state. The parameter values that make true
@@ -41,7 +42,7 @@ preconditions and guards.
corresponds to a deadlock*
[[virtual-operations]]
-==== Virtual Operations
+=== Virtual Operations
There are three particular operations that correspond to specific tasks
performed by ProB:
@@ -64,7 +65,7 @@ pane. These enable the user to explore interactively the behaviour of
the B machine.
[[animating-the-b-machine]]
-==== Animating the B machine
+=== Animating the B machine
If the B machine has constants, one or several initialise constants
operations are displayed. The user selects one of these operations, then
@@ -94,7 +95,7 @@ added to the History pane, the effect of the operation are computed and
the state is updated in the State Properties pane.
[[the-analyse-menu]]
-=== The Analyse menu
+== The Analyse menu
At each point during the animation process, several useful commands
displaying various information on the B machine are available in the
@@ -122,7 +123,7 @@ properties and the Analyse Assertions plays this role for the
assertions.
[[animation-preferences]]
-=== Animation Preferences
+== Animation Preferences
The animation process in ProB can be configured via several preferences
set in the preference window Preferences|Animation Preferences.
@@ -142,7 +143,7 @@ The preference Check invariant will toggle the display of the invariant
status indicator in the State Properties pane.
[[other-animation-features]]
-=== Other Animation Features
+== Other Animation Features
Several other commands are provided by ProB in the _Animate_ menu for
animating B specifications. The Reset command will set the state of the
diff --git a/src/docs/chapter/developer/Building_ProB_on_Windows.adoc b/src/docs/chapter/user/10_General/Building_ProB_on_Windows.adoc
similarity index 100%
rename from src/docs/chapter/developer/Building_ProB_on_Windows.adoc
rename to src/docs/chapter/user/10_General/Building_ProB_on_Windows.adoc
index 20e9686..e263a07 100644
--- a/src/docs/chapter/developer/Building_ProB_on_Windows.adoc
+++ b/src/docs/chapter/user/10_General/Building_ProB_on_Windows.adoc
@@ -1,7 +1,7 @@
+
[[building-prob-on-windows]]
= Building ProB on Windows
-
In case that you want to compile ProB from Source on Windows (XP),
here are some information about the setup:
diff --git a/src/docs/chapter/user/10_General/Colours_of_enabled_operations.adoc b/src/docs/chapter/user/10_General/Colours_of_enabled_operations.adoc
index a1340c4..aa892eb 100644
--- a/src/docs/chapter/user/10_General/Colours_of_enabled_operations.adoc
+++ b/src/docs/chapter/user/10_General/Colours_of_enabled_operations.adoc
@@ -1,5 +1,6 @@
+
[[colours-of-enabled-operations]]
-== Colours of enabled operations
+= Colours of enabled operations
The enabled operations are shown in different colours, depending on the
state where the operation leads to. If more than one rule of the
diff --git a/src/docs/chapter/user/10_General/Controlling_ProB_Preferences.adoc b/src/docs/chapter/user/10_General/Controlling_ProB_Preferences.adoc
index 95afae4..7e3c80a 100644
--- a/src/docs/chapter/user/10_General/Controlling_ProB_Preferences.adoc
+++ b/src/docs/chapter/user/10_General/Controlling_ProB_Preferences.adoc
@@ -1,5 +1,6 @@
+
[[controlling-prob-preferences]]
-== Controlling ProB Preferences
+= Controlling ProB Preferences
ProB provides a variety of preferences to control its behaviour. A list
of the most important preferences can be found
@@ -8,7 +9,7 @@ page for probcli>>. We also have a separate <<deferred-sets,manual
page about setting the sizes of deferred sets>>.
[[setting-preferences-in-a-b-machine]]
-=== Setting Preferences in a B machine
+== Setting Preferences in a B machine
This only works for classical B models. For a preference `P` you can add
the following definition to the `DEFINITIONS` section of the main
@@ -19,7 +20,7 @@ machine:
This will set the preference `P` to the value `VAL` for this model only.
[[setting-preferences-from-the-command-line]]
-=== Setting Preferences from the command-line
+== Setting Preferences from the command-line
You can set a preference `P` to a value `VAL` for a particular run of
probcli by adding the command-line switch `-p P VAL`, e.g.,
@@ -44,7 +45,7 @@ set>> `GS` using the following command-line switch:
`-card GS Val`
[[setting-preferences-from-prob-tcltk]]
-=== Setting Preferences from ProB Tcl/Tk
+== Setting Preferences from ProB Tcl/Tk
ProB Tcl/Tk stores your preferences settings in a file
`ProB_Preferences.pl`.
diff --git a/src/docs/chapter/user/10_General/Current_Limitations.adoc b/src/docs/chapter/user/10_General/Current_Limitations.adoc
index 3e1796e..18d7d32 100644
--- a/src/docs/chapter/user/10_General/Current_Limitations.adoc
+++ b/src/docs/chapter/user/10_General/Current_Limitations.adoc
@@ -1,5 +1,6 @@
+
[[current-limitations]]
-== Current Limitations
+= Current Limitations
ProB in general requires all <<deferred-sets,deferred sets>> to be
given a finite cardinality. If no cardinality is specified, a default
@@ -38,7 +39,7 @@ composition (or other uses of the semicolon).
See the page <<using-prob-with-atelier-b,Using ProB with Atelier B>> for more details.
[[multiple-machines-and-refinements]]
-=== Multiple Machines and Refinements
+== Multiple Machines and Refinements
It is possible to use multiple B machines with ProB. However, ProB may
not enforce all of the classical B visibility rules (although we try
diff --git a/src/docs/chapter/user/10_General/Deferred_Sets.adoc b/src/docs/chapter/user/10_General/Deferred_Sets.adoc
index 94e2751..cff2e16 100644
--- a/src/docs/chapter/user/10_General/Deferred_Sets.adoc
+++ b/src/docs/chapter/user/10_General/Deferred_Sets.adoc
@@ -1,5 +1,6 @@
+
[[deferred-sets]]
-== Deferred Sets
+= Deferred Sets
A deferred set in B is declared in the SETS Section and is not
explicitly enumerated. In the example below, AA is a deferred set and BB
@@ -35,7 +36,7 @@ influence the size used for AA by ProB, for example:
set the cardinality of AA to the constant.
[[using-refinement-for-animation-preferences]]
-=== Using Refinement for Animation Preferences
+== Using Refinement for Animation Preferences
Note: instead of adding AA = \{aa,bb} to the SETS clause you can also
add `AA = {aa,bb} & aa/=bb` to the PROPERTIES clause. This can also be
@@ -52,7 +53,7 @@ END
....
[[setting-deferred-set-cardinalities-within-probcli]]
-=== Setting Deferred Set Cardinalities within probcli
+== Setting Deferred Set Cardinalities within probcli
From the command-line, using probcli you can use the command-line
switch:
diff --git a/src/docs/chapter/user/10_General/Editors_for_ProB.adoc b/src/docs/chapter/user/10_General/Editors_for_ProB.adoc
index 735aaac..532490c 100644
--- a/src/docs/chapter/user/10_General/Editors_for_ProB.adoc
+++ b/src/docs/chapter/user/10_General/Editors_for_ProB.adoc
@@ -1,8 +1,9 @@
+
[[editors-for-prob]]
-== Editors for ProB
+= Editors for ProB
[[prob-tcltk-editor]]
-=== ProB Tcl/Tk Editor
+== ProB Tcl/Tk Editor
ProB Tcl/Tk contains an editor in which syntax errors are displayed and
which can be used to edit B, CSP, Z and TLA+ models. The editor of
@@ -23,7 +24,7 @@ file with this editor. You can also use the command-key shortcut
"Cmd-E" for this.
[[launching-the-editor-in-probcli]]
-=== Launching the editor in probcli
+== Launching the editor in probcli
The <<using-the-command-line-version-of-prob,probcli>> REPL
(read-eval-print-loop) supports the command `:e` to open the current
@@ -36,10 +37,10 @@ In case errors occurred with the last command, this will also try and
move the cursor to the corresponding location in the file.
[[external-editors]]
-=== External Editors
+== External Editors
[[vim]]
-==== VIM
+=== VIM
A https://github.com/bivab/prob.vim[VIM plugin for ProB is available].
It shows a quick fix list of parse and type errors for classical B
@@ -49,7 +50,7 @@ VIM has builtin syntax highlighting support for
https://github.com/vim/vim/blob/master/runtime/syntax/b.vim[B].
[[atom]]
-==== Atom
+=== Atom
There is a package
https://atom.io/packages/language-b-eventb[language-b-eventb] available
@@ -58,12 +59,12 @@ specification languages B and Event-B to Atom. It integrates with
probcli to obtain error markers for syntax and type errors.
[[bbedit]]
-==== BBEdit
+=== BBEdit
Some https://github.com/leuschel/bbedit-prob[BBedit Language modules for
B, TLA+, CSP and Prolog] are available.
[[emacs]]
-==== Emacs
+=== Emacs
A package is available. //TODO: Downloadlink b-mode.el.zip[]
diff --git a/src/docs/chapter/user/10_General/GeneralPresentation.adoc b/src/docs/chapter/user/10_General/GeneralPresentation.adoc
index 0a4bfd3..3532ae5 100644
--- a/src/docs/chapter/user/10_General/GeneralPresentation.adoc
+++ b/src/docs/chapter/user/10_General/GeneralPresentation.adoc
@@ -1,8 +1,9 @@
+
[[general-presentation]]
-== General Presentation
+= General Presentation
[[the-prob-main-window]]
-=== The ProB Main Window
+== The ProB Main Window
The menu bar contains the various commands to access the features of
ProB. It includes the traditional _File_ menu with a sub-menu "Recent
@@ -37,7 +38,7 @@ mean);
3. The history of operations leading to this state (History).
[[general-presentation-preferences]]
-=== Preferences
+== Preferences
The _Preferences_ menu allows the various features of ProB to be
configured. When ProB is started for the first time, it creates a file
diff --git a/src/docs/chapter/developer/Getting_Involved.adoc b/src/docs/chapter/user/10_General/Getting_Involved.adoc
similarity index 100%
rename from src/docs/chapter/developer/Getting_Involved.adoc
rename to src/docs/chapter/user/10_General/Getting_Involved.adoc
index cc0f620..74d943b 100644
--- a/src/docs/chapter/developer/Getting_Involved.adoc
+++ b/src/docs/chapter/user/10_General/Getting_Involved.adoc
@@ -1,7 +1,7 @@
+
[[getting-involved]]
= Getting Involved
-
[[the-prob-java-core-and-ui]]
== The ProB Java Core and UI
diff --git a/src/docs/chapter/user/10_General/ProB_Logic_Calculator_old.adoc b/src/docs/chapter/user/10_General/ProB_Logic_Calculator_old.adoc
index 76a8ec6..bea5ff3 100644
--- a/src/docs/chapter/user/10_General/ProB_Logic_Calculator_old.adoc
+++ b/src/docs/chapter/user/10_General/ProB_Logic_Calculator_old.adoc
@@ -1,5 +1,8 @@
+
[[prob-logic-calculator]]
-== ProB Logic Calculator
+= ProB Logic Calculator
+
+WARNING: This section is relatively old and may contain errors.
Below is a ProB-based http://research.microsoft.com/en-us/um/people/lamport/tla/logic-calculators.html[logic
calculator]. You can enter predicates and expressions in the upper
@@ -28,7 +31,7 @@ versions available for Linux and Mac (the above calculator only uses the
32-bit version).
[[short-syntax-guide-for-b-constructs]]
-=== Short syntax guide for some of B's constructs:
+== Short syntax guide for some of B's constructs:
* comments `/* ... */`
* conjunction `P & Q`, disjunction `P or Q`, implication `P \=> Q`,
@@ -91,7 +94,7 @@ https://www3.hhu.de/stups/downloads/pdf/PlaggeLeuschel_Kodkod2012.pdf[ProB-Kodko
backend] instead of the default constraint-logic programming kernel.
[[small-tutorial]]
-=== Small Tutorial
+== Small Tutorial
Here is a small tutorial to get you started. B distinguishes
expressions, which have a value, and predicates which can be either true
@@ -209,7 +212,7 @@ will refine ProB's output to also indicate when the
solution/counter-example is still guaranteed to be correct)!
[[executing-the-calculator-locally]]
-=== Executing the Calculator locally
+== Executing the Calculator locally
You can evaluate formulas on your machine in the same way as the
calculator above, by <<downloads,downloading ProB>> (ideally a nightly
diff --git a/src/docs/chapter/developer/30_tcltk/ZZ_section_footer.adoc b/src/docs/chapter/user/10_General/ZZ_section_footer.adoc
similarity index 94%
rename from src/docs/chapter/developer/30_tcltk/ZZ_section_footer.adoc
rename to src/docs/chapter/user/10_General/ZZ_section_footer.adoc
index 3b4360c..909c09e 100644
--- a/src/docs/chapter/developer/30_tcltk/ZZ_section_footer.adoc
+++ b/src/docs/chapter/user/10_General/ZZ_section_footer.adoc
@@ -1 +1,2 @@
+
:leveloffset: -1
diff --git a/src/docs/chapter/user/11_BLanguage/00_BLanguage.adoc b/src/docs/chapter/user/11_BLanguage/00_section_header.adoc
similarity index 60%
rename from src/docs/chapter/user/11_BLanguage/00_BLanguage.adoc
rename to src/docs/chapter/user/11_BLanguage/00_section_header.adoc
index ba531e1..39d27f5 100644
--- a/src/docs/chapter/user/11_BLanguage/00_BLanguage.adoc
+++ b/src/docs/chapter/user/11_BLanguage/00_section_header.adoc
@@ -1,2 +1,4 @@
+
[[b-language]]
= B Language
+:leveloffset: +1
diff --git a/src/docs/chapter/user/11_BLanguage/01_Summary_of_B_Syntax.adoc b/src/docs/chapter/user/11_BLanguage/01_Summary_of_B_Syntax.adoc
index 7b8bde0..a81c119 100644
--- a/src/docs/chapter/user/11_BLanguage/01_Summary_of_B_Syntax.adoc
+++ b/src/docs/chapter/user/11_BLanguage/01_Summary_of_B_Syntax.adoc
@@ -1,8 +1,9 @@
+
[[summary-of-b-syntax]]
-== Summary of B Syntax
+= Summary of B Syntax
[[logical-predicates]]
-=== Logical predicates:
+== Logical predicates:
....
P & Q conjunction
@@ -20,7 +21,7 @@ Note: you can also introduce multiple variables inside a universal or
existential quantification, e.g., `!(x,y).(P => Q)`.
[[equality]]
-=== Equality:
+== Equality:
....
E = F equality
@@ -28,7 +29,7 @@ existential quantification, e.g., `!(x,y).(P => Q)`.
....
[[booleans]]
-=== Booleans:
+== Booleans:
....
TRUE
@@ -44,7 +45,7 @@ values `x` and `y` using conjunction you have to write
value you have to use `bool(z>0)`.
[[sets]]
-=== Sets:
+== Sets:
....
{} empty set
@@ -73,7 +74,7 @@ value you have to use `bool(z>0)`.
....
[[numbers]]
-=== Numbers:
+== Numbers:
....
INTEGER set of integers
@@ -104,7 +105,7 @@ value you have to use `bool(z>0)`.
....
[[relations]]
-=== Relations:
+== Relations:
....
S<->T relation
@@ -134,7 +135,7 @@ value you have to use `bool(z>0)`.
....
[[functions]]
-=== Functions:
+== Functions:
....
S+->T partial function
@@ -151,7 +152,7 @@ value you have to use `bool(z>0)`.
....
[[sequences]]
-=== Sequences:
+== Sequences:
....
<> or [] empty sequence
@@ -178,7 +179,7 @@ value you have to use `bool(z>0)`.
....
[[records]]
-=== Records:
+== Records:
....
struct(ID:S,...,ID:S) set of records with given fields and field types
@@ -187,7 +188,7 @@ value you have to use `bool(z>0)`.
....
[[strings]]
-=== Strings:
+== Strings:
....
"astring" a specific (single-line) string value
@@ -219,7 +220,7 @@ tabs and newlines. ProB assumes that all B machines and strings use the
UTF-8 encoding.
[[trees]]
-=== Trees:
+== Trees:
Nodes in the tree are denoted by index sequences (branches), e.g,
n=[1,2,1] Each node in the tree is labelled with an element from a
@@ -248,7 +249,7 @@ domain S.
....
[[let-and-if-then-else]]
-=== LET and IF-THEN-ELSE
+== LET and IF-THEN-ELSE
ProB allows the following for predicates and expressions:
@@ -260,7 +261,7 @@ ProB allows the following for predicates and expressions:
Note: The expressions E1,... defining x1,... are not allowed to use x1,...
[[statements-aka-substitutions]]
-=== Statements (aka Substitutions):
+== Statements (aka Substitutions):
....
skip no operation
@@ -294,7 +295,7 @@ Note: The expressions E1,... defining x1,... are not allowed to use x1,...
....
[[machine-header]]
-=== Machine header:
+== Machine header:
....
MACHINE or REFINEMENT or IMPLEMENTATION
@@ -307,7 +308,7 @@ Note: The expressions E1,... defining x1,... are not allowed to use x1,...
....
[[machine-sections]]
-=== Machine sections:
+== Machine sections:
----
CONSTRAINTS P (logical predicate)
@@ -325,7 +326,7 @@ Note: The expressions E1,... defining x1,... are not allowed to use x1,...
----
[[machine-inclusion]]
-=== Machine inclusion:
+== Machine inclusion:
....
USES list of machines
@@ -343,7 +344,7 @@ Note: The expressions E1,... defining x1,... are not allowed to use x1,...
....
[[definitions]]
-=== Definitions:
+== Definitions:
....
NAME1 == Expression; Definition without arguments
@@ -378,7 +379,7 @@ There are a few Definitions which can be used to influence the animator:
....
[[comments-and-pragmas]]
-=== Comments and Pragmas
+== Comments and Pragmas
....
B supports two styles of comments:
@@ -408,7 +409,7 @@ The whitespace between @ and PRAGMA is optional.
----
[[file-extensions]]
-=== File Extensions
+== File Extensions
....
.mch for abstract machine files
@@ -419,7 +420,7 @@ The whitespace between @ and PRAGMA is optional.
....
[[differences-with-atelierbb4free]]
-=== Differences with AtelierB/B4Free
+== Differences with AtelierB/B4Free
Basically, ProB tries to be compatible with Atelier B and conforms to
the semantics of Abrial's B-Book and of
@@ -466,7 +467,7 @@ AtelierB/ProB:
- In AtelierB/ProB the BOOL type is pre-defined and cannot be redefined
[[other-notes]]
-=== Other notes
+== Other notes
ProB is best at treating universally quantified formulas of the form `!x.(x:SET => RHS)`,
or `!(x,y).(x|->y:SET =>RHS)`, `!(x,y,z).(x|->y|->z:SET =>RHS)`, ...;+
otherwise the treatment of `!(x1,...,xn).(LHS => RHS)` may delay until all values treated by LHS are known. +
diff --git a/src/docs/chapter/user/11_BLanguage/02_Types.adoc b/src/docs/chapter/user/11_BLanguage/02_Types.adoc
index b7306b6..f400fc6 100644
--- a/src/docs/chapter/user/11_BLanguage/02_Types.adoc
+++ b/src/docs/chapter/user/11_BLanguage/02_Types.adoc
@@ -1,5 +1,6 @@
+
[[types]]
-== Types
+= Types
ProB requires all constants and variables to be typed. As of version
1.3, ProB uses a new unification-based type inference and checking
@@ -10,7 +11,7 @@ adding additional typing predicates). Also note that, in contrast to
Atelier B, ProB will type check macro DEFINITIONS.
[[what-is-a-basic-type-in-b]]
-=== What is a basic type in B
+== What is a basic type in B
* BOOL
* INTEGER
@@ -20,7 +21,7 @@ parameter of the machine
* τ1 * τ2 (Cartesian product) for τ1 and τ2 being two types
[[what-needs-to-be-typed]]
-=== What needs to be typed
+== What needs to be typed
Generally speaking, any constant or variable. More precisely:
@@ -46,7 +47,7 @@ ProB will warn you if a variable has not been given a type.
inferred for your constants and global variables.*
[[restriction-on-the-domains-of-the-variables]]
-=== Restriction on the Domains of the Variables
+== Restriction on the Domains of the Variables
Animating and verifying a B specification is in principle undecidable.
ProB overcomes this by requiring that the domain of the variables is
@@ -72,7 +73,7 @@ ProB, provided it is of a simple form `card(S)=Nr`, where `S` is a deferred
set and `Nr` a natural number.
[[enumeration-in-prob]]
-=== Enumeration in ProB
+== Enumeration in ProB
The typing information is used by ProB to enumerate the possible values
of a constant or a variable whenever a specification does not narrow
diff --git a/src/docs/chapter/user/11_BLanguage/10_External_Functions.adoc b/src/docs/chapter/user/11_BLanguage/10_External_Functions.adoc
index 57c2973..6190fff 100644
--- a/src/docs/chapter/user/11_BLanguage/10_External_Functions.adoc
+++ b/src/docs/chapter/user/11_BLanguage/10_External_Functions.adoc
@@ -1,5 +1,6 @@
+
[[external-functions]]
-== External Functions
+= External Functions
As of version 1.3.5-beta7 ProB can make use of externally defined
functions. These functions must currently be written in Prolog (in
@@ -15,7 +16,7 @@ external functions already defined by ProB, then you don't have to
understand this mechanism in detail (or at all).
[[standard-libraries-provided-by-prob]]
-=== Standard Libraries provided by ProB
+== Standard Libraries provided by ProB
In a first instance we have predefined a series of external functions
and grouped them in various library machines and definition files:
@@ -76,7 +77,7 @@ DEFINITIONS
-------------
[[overview-of-the-external-function-definition-mechanism]]
-=== Overview of the External Function DEFINITION Mechanism
+== Overview of the External Function DEFINITION Mechanism
Currently, external functions are linked to classical B machines using B
DEFINITIONS as follows:
diff --git a/src/docs/chapter/user/11_BLanguage/11_Recursively_Defined_Functions.adoc b/src/docs/chapter/user/11_BLanguage/11_Recursively_Defined_Functions.adoc
index 1fefb0d..5acacdb 100644
--- a/src/docs/chapter/user/11_BLanguage/11_Recursively_Defined_Functions.adoc
+++ b/src/docs/chapter/user/11_BLanguage/11_Recursively_Defined_Functions.adoc
@@ -1,8 +1,9 @@
+
[[recursively-defined-functions]]
-== Recursively Defined Functions
+= Recursively Defined Functions
[[symbolic-functions-and-relations]]
-=== Symbolic Functions and Relations
+== Symbolic Functions and Relations
Take the following function:
@@ -113,7 +114,7 @@ You may also want to look at the tutorial page on
<<tutorial-modeling-infinite-datatypes,modeling infinite datatypes>>.
[[when-does-prob-treat-a-set-comprehension-or-lambda-abstraction-symbolically]]
-==== When does ProB treat a set comprehension or lambda abstraction symbolically ?
+=== When does ProB treat a set comprehension or lambda abstraction symbolically ?
Currently there are four cases when ProB tries to keep a function such
as `f = %x.(PRED|E)` symbolically rather than computing an explicit
@@ -137,7 +138,7 @@ database attributes and one should use the
<<tutorial-symbolic-constants,symbolic constants plugin>>.
[[recursive-function-definitions-in-prob]]
-=== Recursive Function Definitions in ProB
+== Recursive Function Definitions in ProB
As of version 1.3.5-beta7 ProB now accepts recursively defined
functions. For this:
@@ -171,7 +172,7 @@ SEND
---------
[[operations-applicable-for-recursive-functions]]
-==== Operations applicable for recursive functions
+=== Operations applicable for recursive functions
With such a recursive function you can:
diff --git a/src/docs/chapter/user/11_BLanguage/20_Tips:_B_Idioms.adoc b/src/docs/chapter/user/11_BLanguage/20_Tips:_B_Idioms.adoc
index 89f560d..20138fe 100644
--- a/src/docs/chapter/user/11_BLanguage/20_Tips:_B_Idioms.adoc
+++ b/src/docs/chapter/user/11_BLanguage/20_Tips:_B_Idioms.adoc
@@ -1,23 +1,23 @@
+
[[tips-b-idioms]]
-== Tips: B Idioms
+= Tips: B Idioms
-Also have a look at
-/Tips:_Writing_Models_for_ProB[Tips:_Writing_Models_for_ProB].
+Also have a look at <<tips-writing-models-for-prob,Tips:_Writing_Models_for_ProB>>.
[[let]]
-=== Let
+== Let
Classical B only has a LET substitution, no let construct for predicates
or expressions. Event-B has no let construct whatsoever.
[[probs-extended-syntax]]
-==== ProB's Extended Syntax
+=== ProB's Extended Syntax
Since version *1.6.1-beta* (28th of April 2016), ProB supports the use
of the `LET` substitution syntax in expressions and predicates.
[[examples-let]]
-===== Examples:
+==== Examples:
----
>>> LET a BE a = 10 IN a + 10 END
@@ -50,7 +50,7 @@ Expression Value = 11
----
[[let-for-predicates]]
-==== Let for predicates
+=== Let for predicates
For predicates this encodes a let predicate:
@@ -81,7 +81,7 @@ both encode
`{x|let y=E1 & z=E2 in P}`
[[let-for-expressions]]
-==== Let for expressions
+=== Let for expressions
In case F is a set expression, then the following construct can be used
to encode a let statement:
@@ -97,19 +97,19 @@ The following construct has exactly the same effect:
`INTER(x).(x=E|F)`
[[if-then-else]]
-=== If-Then-Else
+== If-Then-Else
Classical B only has an IF-THEN-ELSE substitution (aka statement), no
such construct for predicates or expressions.
[[nightly-builds]]
-==== Nightly Builds
+=== Nightly Builds
Since version *1.6.1-beta* (28th of April 2016), ProB supports the use
of the `LET` substitution syntax in expressions and predicates.
[[examples-if-then-else]]
-===== Examples:
+==== Examples:
----
>>> IF 1 = 1 THEN 3 ELSE 4 END
@@ -131,7 +131,7 @@ Predicate is FALSE
Predicate is TRUE
----
[[expressions]]
-==== Expressions
+=== Expressions
The following construct
@@ -148,7 +148,7 @@ parentheses around the IF-THEN-ELSE; version 1.6.1 no longer requires
them).
[[finite]]
-=== finite
+== finite
In classical B there is no counterpart to the Event-B `finite` operator.
However, the following construct has the same effect as `finite(x)` (and
@@ -157,7 +157,7 @@ is recognised by ProB):
`x : FIN(x)`
[[all-different]]
-=== all-different
+== all-different
One can encode the fact that n objects x1,...,xn are pair-wise different
using the following construct (recognised by ProB):
@@ -165,7 +165,7 @@ using the following construct (recognised by ProB):
`card({x1,...,xn})=n`
[[map]]
-=== map
+== map
Given a function f and a sequence `sqce` one can map the function over
all elements of `sqce` using the relational composition operator `;`:
@@ -175,7 +175,7 @@ all elements of `sqce` using the relational composition operator `;`:
For example, `([1,2,3] ; succ)` gives us the sequence `[2,3,4]`.
[[recursion-using-closure1]]
-=== Recursion using closure1
+== Recursion using closure1
Even though B has no built-in support for recursion, one can use the
transitive closure operator `closure1` to compute certain recursive
@@ -214,7 +214,7 @@ can compute the relational image of `closure1(step)` for a particular
set such as `{({4,5,2},[])}` (provided the recursion terminates).
[[recursion-using-abstract_constants]]
-=== Recursion using ABSTRACT:_CONSTANTS
+== Recursion using ABSTRACT:_CONSTANTS
Recursive functions can be declared using the `ABSTRACT_CONSTANTS`
section in B machines. Functions declared as `ABSTRACT_CONSTANTS` are
diff --git a/src/docs/chapter/user/11_BLanguage/21_Tips:_Writing_Models_for_ProB.adoc b/src/docs/chapter/user/11_BLanguage/21_Tips:_Writing_Models_for_ProB.adoc
index bc05247..6fb548d 100644
--- a/src/docs/chapter/user/11_BLanguage/21_Tips:_Writing_Models_for_ProB.adoc
+++ b/src/docs/chapter/user/11_BLanguage/21_Tips:_Writing_Models_for_ProB.adoc
@@ -1,6 +1,6 @@
-[[tips-writing-models-for-prob]]
-== Tips: Writing Models for ProB
+[[tips-writing-models-for-prob]]
+= Tips: Writing Models for ProB
The most common issue is that ProB needs to find values for the
constants which satisfy the properties (aka axioms in Event-B). You
@@ -32,10 +32,10 @@ a function is fine, computing the image over a set is also possible as
is taking the union with another symbolic function.
[[effective-constraint-solving-with-prob]]
-=== Effective Constraint Solving with ProB
+== Effective Constraint Solving with ProB
[[existential-quantifiers]]
-==== Existential Quantifiers
+=== Existential Quantifiers
Existential quantifiers can pose subtle problems when solving constraint
problems.
@@ -73,7 +73,7 @@ avoid repeated computations
elimination>>) and to make your predicates more readable.
[[universal-quantifiers]]
-=== Universal Quantifiers
+== Universal Quantifiers
The situation is very similar to the existential quantifier. In the
worst case ProB may delay evaluating a universal quantifier `!x.(P=>Q)`
@@ -100,7 +100,7 @@ of `1..10`, then we can rewrite `!x.(s(x)=5 => P(x))` into
is checked.
[[transitive-closure-in-event-b]]
-=== Transitive Closure in Event-B
+== Transitive Closure in Event-B
Classical B contains the transitive closure operator `closure1`. It is
not available by default in Event-B, and axiomatisations of it may be
diff --git a/src/docs/chapter/user/11_BLanguage/WD/00_section_header.adoc b/src/docs/chapter/user/11_BLanguage/WD/00_section_header.adoc
new file mode 100644
index 0000000..92a1941
--- /dev/null
+++ b/src/docs/chapter/user/11_BLanguage/WD/00_section_header.adoc
@@ -0,0 +1,4 @@
+
+[[well-definedness]]
+= Well Definedness
+:leveloffset: +1
diff --git a/src/docs/chapter/user/11_BLanguage/WD/01_Well-Definedness_Checking.adoc b/src/docs/chapter/user/11_BLanguage/WD/01_Well-Definedness_Checking.adoc
index 6d28aa6..8690053 100644
--- a/src/docs/chapter/user/11_BLanguage/WD/01_Well-Definedness_Checking.adoc
+++ b/src/docs/chapter/user/11_BLanguage/WD/01_Well-Definedness_Checking.adoc
@@ -1,5 +1,6 @@
+
[[well-definedness-checking]]
-== Well-Definedness Checking
+= Well-Definedness Checking
Well-definedness errors can occur in B in the following circumstances:
diff --git a/src/docs/chapter/developer/10_java_api/ZZ_section_footer.adoc b/src/docs/chapter/user/11_BLanguage/WD/ZZ_section_footer.adoc
similarity index 94%
rename from src/docs/chapter/developer/10_java_api/ZZ_section_footer.adoc
rename to src/docs/chapter/user/11_BLanguage/WD/ZZ_section_footer.adoc
index 3b4360c..909c09e 100644
--- a/src/docs/chapter/developer/10_java_api/ZZ_section_footer.adoc
+++ b/src/docs/chapter/user/11_BLanguage/WD/ZZ_section_footer.adoc
@@ -1 +1,2 @@
+
:leveloffset: -1
diff --git a/src/docs/chapter/developer/20_prolog/ZZ_section_footer.adoc b/src/docs/chapter/user/11_BLanguage/ZZ_section_footer.adoc
similarity index 94%
rename from src/docs/chapter/developer/20_prolog/ZZ_section_footer.adoc
rename to src/docs/chapter/user/11_BLanguage/ZZ_section_footer.adoc
index 3b4360c..909c09e 100644
--- a/src/docs/chapter/developer/20_prolog/ZZ_section_footer.adoc
+++ b/src/docs/chapter/user/11_BLanguage/ZZ_section_footer.adoc
@@ -1 +1,2 @@
+
:leveloffset: -1
diff --git a/src/docs/chapter/user/20_Validation/00_section_header.adoc b/src/docs/chapter/user/20_Validation/00_section_header.adoc
new file mode 100644
index 0000000..af7d604
--- /dev/null
+++ b/src/docs/chapter/user/20_Validation/00_section_header.adoc
@@ -0,0 +1,4 @@
+
+[[validation]]
+= Validation
+:leveloffset: +1
diff --git a/src/docs/chapter/user/20_Validation/CBC/00_section_header.adoc b/src/docs/chapter/user/20_Validation/CBC/00_section_header.adoc
new file mode 100644
index 0000000..0e59252
--- /dev/null
+++ b/src/docs/chapter/user/20_Validation/CBC/00_section_header.adoc
@@ -0,0 +1,19 @@
+
+[[constraint-based-checking]]
+= Constraint Based Checking
+:leveloffset: +1
+
+ProB also offers an alternative checking method, inspired by the Alloy
+footnote:[D. Jackson: Alloy: A lightweight object modeling notation. ACM
+Transactions Software Engineering and Methodology (TOSEM),
+11(2):256–290, 2002.] analyser. In this mode of operation, ProB does not
+explore the reachable states starting from the initial state(s), but
+checks whether applying a single operation can result in a property
+violation (invariant and assertion) independently of the particular
+initialization of the B machine. This is done by symbolic constraint
+solving, and we call this approach constraint based checking (another
+sensible name would be model finding).
+
+More details and examples can be found in the
+<<tutorial-model-checking-proof-and-cbc,tutorial page on model
+checking, proof and CBC>>.
diff --git a/src/docs/chapter/user/20_Validation/CBC/01_Constraint_Based_Checking.adoc b/src/docs/chapter/user/20_Validation/CBC/01_Constraint_Based_Checking.adoc
index 513ffb7..6aa6a0e 100644
--- a/src/docs/chapter/user/20_Validation/CBC/01_Constraint_Based_Checking.adoc
+++ b/src/docs/chapter/user/20_Validation/CBC/01_Constraint_Based_Checking.adoc
@@ -1,23 +1,6 @@
-[[constraint-based-checking]]
-== Constraint Based Checking
-
-ProB also offers an alternative checking method, inspired by the Alloy
-footnote:[D. Jackson: Alloy: A lightweight object modeling notation. ACM
-Transactions Software Engineering and Methodology (TOSEM),
-11(2):256–290, 2002.] analyser. In this mode of operation, ProB does not
-explore the reachable states starting from the initial state(s), but
-checks whether applying a single operation can result in a property
-violation (invariant and assertion) independently of the particular
-initialization of the B machine. This is done by symbolic constraint
-solving, and we call this approach constraint based checking (another
-sensible name would be model finding).
-
-More details and examples can be found in the
-<<tutorial-model-checking-proof-and-cbc,tutorial page on model
-checking, proof and CBC>>.
[[difference-between-constraint-based-checking-and-model-checking]]
-=== Difference between Constraint Based Checking and Model Checking
+= Difference between Constraint Based Checking and Model Checking
<<consistency-checking,Model checking>> tries to find a sequence of
operations that, starting from an initial state, leads to a state which
@@ -37,7 +20,7 @@ A comparison between all <<prob-validation-methods,ProB validation
methods can be found on a separate manual section>>.
[[commands-of-the-constraint-based-checker]]
-=== Commands of the Constraint Based Checker
+= Commands of the Constraint Based Checker
These commands are only accessible in the "Normal" mode of ProB (see
<<the-prob-main-window,the general
@@ -71,4 +54,4 @@ The following command is related to the above:
* <<using-the-command-line-version-of-prob,cbc_sequence>> to find a sequence of operations using the constraint solver
-=== References
+= References
diff --git a/src/docs/chapter/user/20_Validation/CBC/10_Bounded_Model_Checking.adoc b/src/docs/chapter/user/20_Validation/CBC/10_Bounded_Model_Checking.adoc
index f0ecea7..9527e16 100644
--- a/src/docs/chapter/user/20_Validation/CBC/10_Bounded_Model_Checking.adoc
+++ b/src/docs/chapter/user/20_Validation/CBC/10_Bounded_Model_Checking.adoc
@@ -1,5 +1,6 @@
+
[[bounded-model-checking]]
-== Bounded Model Checking
+= Bounded Model Checking
As of version 1.5, ProB provides support for constraint-based bounded
model checking (BMC). As opposed to
diff --git a/src/docs/chapter/user/20_Validation/CBC/20_Symbolic_Model_Checking.adoc b/src/docs/chapter/user/20_Validation/CBC/20_Symbolic_Model_Checking.adoc
index b743823..a6f2a33 100644
--- a/src/docs/chapter/user/20_Validation/CBC/20_Symbolic_Model_Checking.adoc
+++ b/src/docs/chapter/user/20_Validation/CBC/20_Symbolic_Model_Checking.adoc
@@ -1,8 +1,9 @@
+
[[symbolic-model-checking]]
-== Symbolic Model Checking
+= Symbolic Model Checking
[[overview-symbolic-model-checking]]
-=== Overview
+== Overview
The current nightly builds of ProB support different symbolic model
checking algorithms:
@@ -26,7 +27,7 @@ checking algorithm based on a different technique is available in Prob.
See <<bounded-model-checking,its wiki page>> for details.
[[usage]]
-=== Usage
+== Usage
Take the following example:
@@ -85,7 +86,7 @@ The algorithms are also available from within ProB Tcl/Tk. They can be
found inside the "Symbolic Model Checking" sub-menu of the _Analyse_ menu.
[[more-details]]
-=== More details
+== More details
A paper describing the symbolic model checking algorithms and how they
are applied to B and Event-B machines has been submitted to ABZ 2016.
diff --git a/src/docs/chapter/user/20_Validation/CBC/ZZ_section_footer.adoc b/src/docs/chapter/user/20_Validation/CBC/ZZ_section_footer.adoc
new file mode 100644
index 0000000..909c09e
--- /dev/null
+++ b/src/docs/chapter/user/20_Validation/CBC/ZZ_section_footer.adoc
@@ -0,0 +1,2 @@
+
+:leveloffset: -1
diff --git a/src/docs/chapter/user/20_Validation/MC/00_section_header.adoc b/src/docs/chapter/user/20_Validation/MC/00_section_header.adoc
new file mode 100644
index 0000000..11b94be
--- /dev/null
+++ b/src/docs/chapter/user/20_Validation/MC/00_section_header.adoc
@@ -0,0 +1,4 @@
+
+[[model-checking]]
+= Model Checking
+:leveloffset: +1
diff --git a/src/docs/chapter/user/20_Validation/MC/01_Consistency_Checking.adoc b/src/docs/chapter/user/20_Validation/MC/01_Consistency_Checking.adoc
index 5bb6adc..37e3eec 100644
--- a/src/docs/chapter/user/20_Validation/MC/01_Consistency_Checking.adoc
+++ b/src/docs/chapter/user/20_Validation/MC/01_Consistency_Checking.adoc
@@ -1,8 +1,9 @@
+
[[consistency-checking]]
-== Model Checking Consistency
+= Model Checking Consistency
[[checking-consistency-via-model-checking]]
-=== Checking Consistency via Model Checking
+== Checking Consistency via Model Checking
By manually animating a B machine, it is possible to discover problems
with the specification, such as invariant violations or deadlocks. The
@@ -19,7 +20,7 @@ spaces and will then explore the state space until it finds an error or
runs out of memory.
[[basics]]
-==== Basics
+=== Basics
During the initial draft of a specification, it is often useful to
utilize the model checker to determine if there are any invariant
@@ -53,7 +54,7 @@ model checker does find errors quite quickly. On that basis, it remains
a useful tool even for specifications whose state space is infinite.
[[using-the-model-checker]]
-==== Using the Model Checker
+=== Using the Model Checker
To model check a B machine loaded in ProB, launch the command from
"Verify| Model Check".
@@ -91,7 +92,7 @@ entire state space has been checked. The user can interrupt the model
checking at any time by pressing the "Cancel" button.
[[incremental-model-checking]]
-===== Incremental Model Checking
+==== Incremental Model Checking
It is important to understand that the computation of and search in the
state space is an incremental process. The model checking can be done by
@@ -120,7 +121,7 @@ the change of the model checking settings may not affect the state space
already computed.
[[results-of-the-model-checking]]
-===== Results of the Model Checking
+==== Results of the Model Checking
When the state space has been computed by ProB, the pop-up window is
replaced by a dialog window stating "No error state found". All new
@@ -137,7 +138,7 @@ property violation) in the "Enabled Operations" pane, and the trace
pane.
[[preferences-of-the-model-checking]]
-===== Preferences of the Model Checking
+==== Preferences of the Model Checking
The preferences "Nr of Initialisations shown" and "Max Number of
Enablings shown" (described in
@@ -165,7 +166,7 @@ Specification and Development in Z and B, LNCS 3455. Springer-Verlag,
https://www3.hhu.de/stups/downloads/pdf/LeTu05_8.pdf].
[[machines-with-invariant-violations-and-deadlocks]]
-==== Machines with Invariant Violations and Deadlocks
+=== Machines with Invariant Violations and Deadlocks
When the two properties (invariant and deadlock-freeness) are checked
and a state violates both, only the invariant violation is reported. In
@@ -186,7 +187,7 @@ simply compute the entire state space until the user presses the Cancel
button or until the specified number of nodes is reached.*
[[two-phase-verification]]
-===== Two Phase Verification
+==== Two Phase Verification
If the state space of the specification can be exhaustively searched,
check for deadlocks and invariant violations in two phases. To do this,
@@ -204,7 +205,7 @@ HINT: At any time during animation and model checking, the user can
reopen the the B specification to purge the state space.
[[interleaved-deadlock-and-invariant-violation-checking]]
-===== Interleaved deadlock and invariant violation checking
+==== Interleaved deadlock and invariant violation checking
If you wish to determine if an already encountered invariant violation
is also a deadlocked node, turn the option "Inspect Existing Nodes"
@@ -217,7 +218,7 @@ WARNING: Enabling "Inspect Existing Nodes" will continually report
the first error it encounters until that error is corrected.
[[specifying-goals-and-assertions]]
-=== Specifying Goals and Assertions
+== Specifying Goals and Assertions
The ASSERTIONS clause of a B machine enables the user to define
predicates that are supposed to be deducible from the INVARIANT or
@@ -242,4 +243,4 @@ a goal without defining it explicitly in the B specification. The
directly in a text field. ProB then searches for a state of the state
space currently computed that satisfies this goal.
-=== References
+== References
diff --git a/src/docs/chapter/user/20_Validation/MC/10_Distributed_Model_Checking.adoc b/src/docs/chapter/user/20_Validation/MC/10_Distributed_Model_Checking.adoc
index 183b9df..3a98ff3 100644
--- a/src/docs/chapter/user/20_Validation/MC/10_Distributed_Model_Checking.adoc
+++ b/src/docs/chapter/user/20_Validation/MC/10_Distributed_Model_Checking.adoc
@@ -1,12 +1,13 @@
+
[[distributed-model-checking]]
-== Distributed Model Checking
+= Distributed Model Checking
Distributed Model Checking allows to check invariants and
deadlock-freedom (and assertions) with additional computational power.
The distributed version of ProB is named _distb_. In the following, we
will document how to run it.
-=== Overview
+== Overview
_distb_ consists of three components.
@@ -19,7 +20,7 @@ is close to the amount of available (physical) CPU cores of a
participating machine.
[[setting-up-shared-memory]]
-=== Setting up shared memory
+== Setting up shared memory
It might be necessary to increase the limits of how much shared memory
may be allocated, both per segment and overall. This is, to our
@@ -45,7 +46,7 @@ sudo sysctl -w kern.sysv.shmseg=4096
sudo sysctl -w kern.sysv.shmall=18446744073692774399
----
-=== Running _distb_
+== Running _distb_
Run once per machine:
@@ -64,7 +65,7 @@ Run as many workers as you want:
`/path/to/prob/probcli -zmq_worker <unique identifier> &`
-=== Additional Preferences
+== Additional Preferences
You can fine-tune the following parameters by adding `-p NAME VALUE` to
the corresponding call (e.g.: `./probcli -zmq_worker worker1 -p port 5010
diff --git a/src/docs/chapter/user/20_Validation/MC/11_DMC.adoc b/src/docs/chapter/user/20_Validation/MC/11_DMC.adoc
index 3000e17..a17d0cc 100644
--- a/src/docs/chapter/user/20_Validation/MC/11_DMC.adoc
+++ b/src/docs/chapter/user/20_Validation/MC/11_DMC.adoc
@@ -1,4 +1,6 @@
-== Distributed Model Checking : Experimental evaluation
+
+[[distributed-model-checking-experimental-evaluation]]
+= Distributed Model Checking : Experimental evaluation
We used three different setups to evaluate the distributed version of ProB.
@@ -6,14 +8,14 @@ We used three different setups to evaluate the distributed version of ProB.
* Amazon EC2 Instances
* The HILBERT cluster
-=== Multicore Computer
+== Multicore Computer
We used a hexacore 3.33GHz Mac Pro with 16GB of RAM. On this computer we
benchmarked all models regardless whether we expected them to be
scalable or not. We varied the number of used cores from 1 up to 12
hyperthreads. Each experiment was repeated at least 5 times.
-=== Amazon EC2 Instances
+== Amazon EC2 Instances
We used c3.8xlarge instances, each of which has 32 virtual CPUs and is
equipped with 64 GB of RAM. We used the Mac Pro to get an impression if
@@ -24,7 +26,7 @@ the Mac Pro were not considered as they would not scale on more
processors. We used 2 or 4 instances connected with 10 GBit ethernet
connection. Each experiment was repeated at least 5 times.
-=== HILBERT
+== HILBERT
We used the high performance cluster at the university of Düsseldorf
(HILBERT) for a single model. The model could not be cheked using a
@@ -36,13 +38,13 @@ executed the experiments once but all experiments on the other platforms
indicated that the variation between experiments could be ignored. Also
the execution times of all 6 experiments seem to be consistent.
-=== Models
+== Models
We cannot make all models public, because they we provided by industrial
partners from various research projects. The models that could be make
available can be downloaded https://www3.hhu.de/stups/models/parb/[here].
-=== Results
+== Results
The results of the experiments are shown in Jens Bendisposto's
dissertation. The dissertation is available https://docserv.uni-duesseldorf.de/servlets/DocumentServlet?id=34472[here].
diff --git a/src/docs/chapter/user/20_Validation/MC/12_ParB.adoc b/src/docs/chapter/user/20_Validation/MC/12_ParB.adoc
index ae38507..a65002b 100644
--- a/src/docs/chapter/user/20_Validation/MC/12_ParB.adoc
+++ b/src/docs/chapter/user/20_Validation/MC/12_ParB.adoc
@@ -1,5 +1,6 @@
+
[[parb]]
-== ParB
+= ParB
This page explains how to run the distributed model checking prototype.
@@ -37,7 +38,7 @@ Example usage:
`$ ./parB.sh 2 ~/parB.log scheduler.mch`
[[running-in-the-cloudcluster]]
-=== Running in the Cloud/Cluster
+== Running in the Cloud/Cluster
The script can only be used for computation on a single physical
computer. If you want to use multiple computers, the setup is a bit more
@@ -71,7 +72,7 @@ logical network in a more convenient way and running the model checker
from within ProB.
[[options-for-parb]]
-=== Options
+== Options
You can use preferences in parB.sh (and the master) :
@@ -85,7 +86,7 @@ otherwise parB will explore the full state space (up to the maximal
number of states)
[[cleaning-up]]
-=== Cleaning up
+== Cleaning up
If something goes wrong it may be necessary to clean up your shared
memory. You can find out if there are still memory blocks occupied using
diff --git a/src/docs/chapter/user/20_Validation/MC/20_LTL_Model_Checking.adoc b/src/docs/chapter/user/20_Validation/MC/20_LTL_Model_Checking.adoc
index 44d4124..eb16c2c 100644
--- a/src/docs/chapter/user/20_Validation/MC/20_LTL_Model_Checking.adoc
+++ b/src/docs/chapter/user/20_Validation/MC/20_LTL_Model_Checking.adoc
@@ -1,5 +1,6 @@
+
[[ltl-model-checking]]
-== LTL Model Checking
+= LTL Model Checking
ProB provides
support for LTL (linear temporal logic) model checking. For an
@@ -65,7 +66,7 @@ The old LTL and CTL dialogs can be accessed from "OldLtlViewers" in
the menu bar.
[[ltl-preferences]]
-=== LTL Preferences
+== LTL Preferences
There is a set of options coming with the LTL model checker. In this
section we give a brief overview of the preferences. The LTL preferences
@@ -126,7 +127,7 @@ Note: Whereas `Y true` is always false when checked with option 1 or 2,
it is usually true (but not in all cases) for option 3.
[[supported-syntax]]
-==== Supported Syntax
+=== Supported Syntax
ProB supports LTL^[e]^, an extended version of LTL. In contrast to the
standard LTL, LTL^[e]^ provides also support for propositions on
@@ -195,7 +196,7 @@ the operations starts.
** `SEF`: strong fairness for all possible operations
[[setting-fairness-constraints]]
-=== Setting Fairness Constraints
+== Setting Fairness Constraints
Fairness is a notion where the search for counterexamples is restricted
to paths that do not ignore infinitely the execution of a set of enabled
@@ -274,7 +275,7 @@ sfair ::= sf(a) | ( sfair ) | sfair & sfair | sfair or sfair
where "a" is a transition proposition.
[[storing-ltl-assertions-in-the-model]]
-=== Storing LTL Assertions in the Model
+== Storing LTL Assertions in the Model
*Storing LTL formulas in B machines* +
LTL formulas can be stored in the DEFINITIONS section of a B machine.
@@ -320,7 +321,7 @@ where `P` is an arbitrary process and `ltl-formula` an LTL formula.
[[ltl-formulas-in-a-separate-file]]
-=== LTL Formulas in a Separate File
+== LTL Formulas in a Separate File
With the command line version of ProB it is possible to check several
LTL^[e]^ formulae with one call. The command has the following syntax:
@@ -343,7 +344,7 @@ One also can check a single LTL^[e]^ formula _F_ using the option
`probcli -ltlformula "F"...`
[[ltl-formulae-in-a-separate-file]]
-=== LTL Formulae in a Separate File
+== LTL Formulae in a Separate File
With the command line version of ProB it is possible to check several
LTL^[e]^ formulae with one call. The command has the following syntax:
@@ -366,7 +367,7 @@ One also can check a single LTL^[e]^ formula _F_ using the option
`probcli -ltlformula "F"...`
[[ltl-model-checker-output]]
-=== LTL Model Checker Output
+== LTL Model Checker Output
The output provided by the LTL model checker can sometimes reveal some
interesting statistical facts about the model and the property being
@@ -511,7 +512,7 @@ a counter-example for "GF [eat.0]" in case no fairness constraints
were imposed.
[[other-relevant-tutorials-about-ltl-model-checking]]
-=== Other Relevant Tutorials about LTL Model Checking
+== Other Relevant Tutorials about LTL Model Checking
A brief tutorial on visualizing LTL counter-examples in the Rodin tool
can be found <<tutorial-ltl-counter-example-view,here>>.
@@ -520,4 +521,4 @@ A tutorial of a simple case study, where setting fairness constraints to
some of the LTL properties is required, can be found
<<mutual-exclusion-fairness,here>>.
-=== References
+== References
diff --git a/src/docs/chapter/user/20_Validation/MC/30_Symmetry_Reduction.adoc b/src/docs/chapter/user/20_Validation/MC/30_Symmetry_Reduction.adoc
index 34450c6..69c0ef1 100644
--- a/src/docs/chapter/user/20_Validation/MC/30_Symmetry_Reduction.adoc
+++ b/src/docs/chapter/user/20_Validation/MC/30_Symmetry_Reduction.adoc
@@ -1,10 +1,11 @@
+
[[symmetry-reduction]]
-== Symmetry Reduction
+= Symmetry Reduction
ProB can make use of symmetries induced
by the use of deferred sets in B (and given sets in Z).
-=== Static Symmetry Reduction
+== Static Symmetry Reduction
ProB will perform a limited form of symmetry reduction for constants
which are elements of deferred sets. Take the following example:
@@ -84,7 +85,7 @@ A = {D1,D2,D3}
B = {D4,D5,D6}
----
-=== Symmetry Reduction during Model Checking
+== Symmetry Reduction during Model Checking
In addition to the above, you can also turn of stronger symmetry
reduction for model checking.
@@ -128,4 +129,4 @@ Proceedings International Symmetry Conference,Januar,2007,Verlag,
https://www3.hhu.de/stups/downloads/pdf/LeMa07_212.pdf].
This is typically the most efficient method.
-=== References
+== References
diff --git a/src/docs/chapter/user/20_Validation/MC/40_LTSmin b/src/docs/chapter/user/20_Validation/MC/40_LTSmin
index 9c1fd00..8cebdad 100644
--- a/src/docs/chapter/user/20_Validation/MC/40_LTSmin
+++ b/src/docs/chapter/user/20_Validation/MC/40_LTSmin
@@ -1,4 +1,6 @@
-== LTSmin Extension
+
+[[lts-min-extension]]
+= LTSmin Extension
In order to set up LTSmin, do the following:
diff --git a/src/docs/chapter/user/20_Validation/MC/ZZ_section_footer.adoc b/src/docs/chapter/user/20_Validation/MC/ZZ_section_footer.adoc
new file mode 100644
index 0000000..909c09e
--- /dev/null
+++ b/src/docs/chapter/user/20_Validation/MC/ZZ_section_footer.adoc
@@ -0,0 +1,2 @@
+
+:leveloffset: -1
diff --git a/src/docs/chapter/user/20_Validation/00_ProB_Validation_Methods.adoc b/src/docs/chapter/user/20_Validation/ProB_Validation_Methods.adoc
similarity index 99%
rename from src/docs/chapter/user/20_Validation/00_ProB_Validation_Methods.adoc
rename to src/docs/chapter/user/20_Validation/ProB_Validation_Methods.adoc
index f666ae8..f0a097e 100644
--- a/src/docs/chapter/user/20_Validation/00_ProB_Validation_Methods.adoc
+++ b/src/docs/chapter/user/20_Validation/ProB_Validation_Methods.adoc
@@ -1,3 +1,4 @@
+
[[prob-validation-methods]]
= ProB Validation Methods
diff --git a/src/docs/chapter/user/20_Validation/Refinement_Checking.adoc b/src/docs/chapter/user/20_Validation/Refinement_Checking.adoc
index 147bf53..8ad9ad9 100644
--- a/src/docs/chapter/user/20_Validation/Refinement_Checking.adoc
+++ b/src/docs/chapter/user/20_Validation/Refinement_Checking.adoc
@@ -1,5 +1,6 @@
+
[[refinement-checking]]
-== Refinement Checking
+= Refinement Checking
ProB can be used for refinement checking
of B, Z and CSP specifications. Below we first discuss refinement
@@ -8,7 +9,7 @@ in ProB which can be viewed
http://stups.hhu.de/ProB/w/Checking_CSP_Assertions[here].
[[what-kind-of-refinement-is-checked]]
-=== What kind of refinement is checked?
+== What kind of refinement is checked?
ProB checks trace refinement. In other words, it checks whether every
trace (consisting of executed operations with their parameter values and
@@ -22,7 +23,7 @@ refinement checking has to be used with care for classical B machines,
but it is well suited for EventB-style machines.
[[how-does-it-work-refinement-checking]]
-=== How does it work?
+== How does it work?
1. Open the abstract specification, explore its state space (e.g.,using
an exhaustive temporal model check).
diff --git a/src/docs/chapter/user/20_Validation/ZZ_section_footer.adoc b/src/docs/chapter/user/20_Validation/ZZ_section_footer.adoc
new file mode 100644
index 0000000..909c09e
--- /dev/null
+++ b/src/docs/chapter/user/20_Validation/ZZ_section_footer.adoc
@@ -0,0 +1,2 @@
+
+:leveloffset: -1
diff --git a/src/docs/chapter/user/21_Testing/00_Testing.adoc b/src/docs/chapter/user/21_Testing/00_section_header.adoc
similarity index 55%
rename from src/docs/chapter/user/21_Testing/00_Testing.adoc
rename to src/docs/chapter/user/21_Testing/00_section_header.adoc
index f7cdbaa..b5ac8d9 100644
--- a/src/docs/chapter/user/21_Testing/00_Testing.adoc
+++ b/src/docs/chapter/user/21_Testing/00_section_header.adoc
@@ -1,2 +1,4 @@
+
[[testing]]
= Testing
+:leveloffset: +1
diff --git a/src/docs/chapter/user/21_Testing/10_State_Space_Coverage_Analyses.adoc b/src/docs/chapter/user/21_Testing/10_State_Space_Coverage_Analyses.adoc
index 4eec949..e8fa3a7 100644
--- a/src/docs/chapter/user/21_Testing/10_State_Space_Coverage_Analyses.adoc
+++ b/src/docs/chapter/user/21_Testing/10_State_Space_Coverage_Analyses.adoc
@@ -1,5 +1,6 @@
+
[[state-space-coverage-analyses]]
-== State Space Coverage Analyses
+= State Space Coverage Analyses
ProB provides various ways to analyse the coverage of the state space of
a model. In ProB Tcl/Tk these features reside in the Coverage submenu of
@@ -48,7 +49,7 @@ The commands to determine vacuous guards and invariants rely on MC/DC
coverage, which is detailed below.
[[mcdc-coverage]]
-=== MC/DC Coverage
+== MC/DC Coverage
MC/DC (Modified Condition/Decision Coverage) is a coverage criterion
which is used in avionics. One core idea is ensure that for every
diff --git a/src/docs/chapter/user/21_Testing/11_Test_Case_Generation.adoc b/src/docs/chapter/user/21_Testing/11_Test_Case_Generation.adoc
index 3365cce..87e0b2f 100644
--- a/src/docs/chapter/user/21_Testing/11_Test_Case_Generation.adoc
+++ b/src/docs/chapter/user/21_Testing/11_Test_Case_Generation.adoc
@@ -1,8 +1,9 @@
+
[[test-case-generation]]
-== Test Case Generation
+= Test Case Generation
[[introduction-to-test-case-generation]]
-=== Introduction
+== Introduction
Testing aims at finding errors in a system or program. A set of tests is
also called a test suite. Test case generation is the process of
@@ -61,11 +62,11 @@ state space is finite it may run forever in case an operation cannot be
covered (because it is infeasible).
[[model-checking-based-test-case-generation]]
-=== Model-Checking-Based Test Case Generation
+== Model-Checking-Based Test Case Generation
Model-checking-based test case generation will build the model's state space, starting from the initial states, until the coverage criterion is satisfied. ProB uses a "breadth-first" approach to search for the test cases.
-==== How to run
+=== How to run
We will use the following B Machine as an example, which is stored in a
file called `simplecounter.mch`.
@@ -87,7 +88,7 @@ END
To start the test case generation there are two alternatives: Using the tcl/tk-application or the command line.
-===== From the command line
+==== From the command line
From the command line there are two commands to configure the
test case generation:
@@ -132,7 +133,7 @@ variables and constants where more than one possible initialisation
exists are written into the trace file, as argument of an INITIALISATION
event.
-===== In the tcl/tk-application
+==== In the tcl/tk-application
In the tcl/tk-application the test case generation can be started by choosing _Analyse_ > "Testing" > "model-checking-based test case generation...". In the appearing window one can set the same parameters as described for the command line.
@@ -157,7 +158,7 @@ You cannot look at the test cases in ProB. Instead you can open the file you jus
....
[[constraint-based-test-case-generation]]
-=== Constraint-Based Test Case Generation
+== Constraint-Based Test Case Generation
Constraint based test case generation allows to explore the state space
for a machine and generate traces of operations that cover certain user
@@ -178,7 +179,7 @@ typically grows exponentially with the depth of the feasible execution
paths.
[[example-when-constraint-based-test-case-generation-is-better]]
-==== Example: When Constraint-based Test Case Generation is better
+=== Example: When Constraint-based Test Case Generation is better
Here is an example which illustrates when constraint-based test case
generation is better.
@@ -240,12 +241,12 @@ no state where BothOverflow is enabled):
image::CBC_StateSpace_Example1.png[]
[[how-to-run]]
-==== How to run
+=== How to run
We will again use the machine `simplecounter.mch`. To start the test case generation there are three alternatives: Using the tcl/tk-application or using the command line by either providing all settings as command line arguments or in a test description file.
-===== From the command line
+==== From the command line
From the command line there are six relevant settings to configure the
test case generation:
@@ -288,7 +289,7 @@ The generated test cases are stored in a file called `test_results.xml`.
Just as with model-checking-based test case generation you can provide the empty filename `''`, in which case no file is generated, and an empty `EndPredicate` that will only lead to test cases of length 1.
[[with-a-test-description-file]]
-===== With a test description file
+==== With a test description file
The configuration for the test case generation can also be provided as
an XML file. The format is shown below:
@@ -339,7 +340,7 @@ with the following call.
./probcli.sh simplecounter.mch -test_description simple_counter_test_description.xml
....
-===== In the tcl/tk-application
+==== In the tcl/tk-application
In the tcl/tk-application the test case generation can be started by choosing _Analyse > Testing > constraint-based test case generation..._. In the appearing window one can set the same parameters as described for the command line.
diff --git a/src/docs/chapter/user/21_Testing/20_Tutorial_Model-Based_Testing.adoc b/src/docs/chapter/user/21_Testing/20_Tutorial_Model-Based_Testing.adoc
index f87464a..3b9610d 100644
--- a/src/docs/chapter/user/21_Testing/20_Tutorial_Model-Based_Testing.adoc
+++ b/src/docs/chapter/user/21_Testing/20_Tutorial_Model-Based_Testing.adoc
@@ -1,5 +1,6 @@
+
[[tutorial-model-based-testing]]
-== Tutorial Model-Based Testing
+= Tutorial Model-Based Testing
We assume that you have completed
<<tutorial-complete-model-checking,Tutorial Complete Model
@@ -36,7 +37,7 @@ There are two ways this coverage can be achieved systematically: using a
model-checking-based or a constraint-based approach.
[[model-checking-based-testcase-generation]]
-=== Model-Checking Based Test Case Generation
+== Model-Checking Based Test Case Generation
To start the test case generation select _Analyse_ > "Testing" > "model-checking-based test case generation...". In the appearing window one can set some parameters:
@@ -98,7 +99,7 @@ You cannot look at the test cases in ProB. Instead you can open the file you jus
[[constraint-based-testcase-generation]]
-=== Constraint-Based Test Case Generation
+== Constraint-Based Test Case Generation
The constraint-based test case generation can be started by selecting _Analyse_ > "Testing" > "constraint-based test case generation...". In the appearing window one can set the same parameters as described before (except for the maximum number of states). Clicking on _"View CBC Test Tree"_ in the window popping up will open another window showing the test cases.
diff --git a/src/docs/chapter/user/21_Testing/ZZ_section_footer.adoc b/src/docs/chapter/user/21_Testing/ZZ_section_footer.adoc
new file mode 100644
index 0000000..909c09e
--- /dev/null
+++ b/src/docs/chapter/user/21_Testing/ZZ_section_footer.adoc
@@ -0,0 +1,2 @@
+
+:leveloffset: -1
diff --git a/src/docs/chapter/user/22_Visualisation/00_Visualisation.adoc b/src/docs/chapter/user/22_Visualisation/00_section_header.adoc
similarity index 65%
rename from src/docs/chapter/user/22_Visualisation/00_Visualisation.adoc
rename to src/docs/chapter/user/22_Visualisation/00_section_header.adoc
index 9c6ba91..cabf81b 100644
--- a/src/docs/chapter/user/22_Visualisation/00_Visualisation.adoc
+++ b/src/docs/chapter/user/22_Visualisation/00_section_header.adoc
@@ -1,2 +1,4 @@
+
[[visualisation]]
= Visualisation
+:leveloffset: +1
diff --git a/src/docs/chapter/user/22_Visualisation/10_Graphical_Viewer.adoc b/src/docs/chapter/user/22_Visualisation/10_Graphical_Viewer.adoc
index 16bdf81..c6b00bc 100644
--- a/src/docs/chapter/user/22_Visualisation/10_Graphical_Viewer.adoc
+++ b/src/docs/chapter/user/22_Visualisation/10_Graphical_Viewer.adoc
@@ -1,9 +1,9 @@
[[graphical-viewer]]
-== Graphical Viewer
+= Graphical Viewer
[[introduction-to-graphical-viewer]]
-=== Introduction
+== Introduction
ProB can generate a wide range of visualizations for your models, e.g.:
@@ -21,7 +21,7 @@ file with the ".ps" extension), or it uses a Dot-Viewer (such as
"dotty") to view the file directly.
[[setting-up-the-graphical-viewer]]
-=== Setting up the Graphical Viewer
+== Setting up the Graphical Viewer
* GraphViz: in order to make use of the graphical visualization
features, you need to install a version of GraphViz suitable for your
diff --git a/src/docs/chapter/user/22_Visualisation/20_State_Space_Visualization.adoc b/src/docs/chapter/user/22_Visualisation/20_State_Space_Visualization.adoc
index bec97b2..2b544f0 100644
--- a/src/docs/chapter/user/22_Visualisation/20_State_Space_Visualization.adoc
+++ b/src/docs/chapter/user/22_Visualisation/20_State_Space_Visualization.adoc
@@ -1,5 +1,6 @@
+
[[state-space-visualization]]
-== State Space Visualization
+= State Space Visualization
ProB provides
several user-friendly visualization features to help the user to analyze
@@ -27,7 +28,7 @@ currently explored by the animation in a separate window.
image::Visualising_the_state_space.png[]
[[graph-nodes]]
-=== Graph Nodes
+== Graph Nodes
ProB displays the state space as a graph whose nodes correspond to
states that are differentiated by their shapes and colors and arcs
@@ -54,7 +55,7 @@ DEFINITION `GOAL == P` or by using a command such as "Find state
satisfying predicate...") then those predicates are coloured in orange.
[[statespace-projections]]
-=== Statespace Projections
+== Statespace Projections
The sub-menu "Statespace Projections" contains several other commands
that provide useful views on the state space.
@@ -85,7 +86,7 @@ effectively. Some sample
here>>
[[other-visualization-commands]]
-=== Other Visualization Commands
+== Other Visualization Commands
The "Visualize" menu contains several other sub-menus, to visualize
traces and individual states. The command "Shortest Trace to Current
@@ -94,7 +95,7 @@ starting from the root node and leading to the current node. The command
"Current State" displays the current node and its successor nodes.
[[preferences-of-the-visualization]]
-=== Preferences of the Visualization
+== Preferences of the Visualization
Many aspects of the visualization can be configured in the "Graphical
Viewer Preferences"... preference window of the "Preferences" menu.
@@ -142,4 +143,4 @@ which is useful for examining large graphs.
* Against Dotty: Dotty may crash if the graph is too big or complex (and
on Solaris and Linux if non-standard mouse buttons are used).
-=== References
+== References
diff --git a/src/docs/chapter/user/22_Visualisation/21_State_space_visualization_examples.adoc b/src/docs/chapter/user/22_Visualisation/21_State_space_visualization_examples.adoc
index 48d42d3..89164bb 100644
--- a/src/docs/chapter/user/22_Visualisation/21_State_space_visualization_examples.adoc
+++ b/src/docs/chapter/user/22_Visualisation/21_State_space_visualization_examples.adoc
@@ -1,8 +1,9 @@
+
[[state-space-visualization-examples]]
-== State space visualization examples
+= State space visualization examples
[[alternating-bit-protocol]]
-=== Alternating Bit Protocol
+== Alternating Bit Protocol
This is a visualisation of 3643 states and 11115 transitions of a TLA+
model of the alternating bit protocol, as distributed with the
@@ -40,7 +41,7 @@ SeqConstraint == /\ Len(msgQ) \leq msgQLen
/\ Len(ackQ) \leq ackQLen
SentLeadsToRcvd == \A d \in Data : (sent = d) /\ (sBit # sAck) ~> (rcvd = d)
-==============================================================================
+=============================================================================
ImpliedAction == [ABCNext]_cvars
@@ -50,11 +51,11 @@ TProp == \A d \in Data : (sent = d) => [](sent = d)
CSpec == ABSpec /\ TNext
DataPerm == Permutations(Data)
-===============================================================
+==============================================================
....
[[mcinnerfifo]]
-=== MCInnerFIFO
+== MCInnerFIFO
This is a visualisation of 3866 states and 9661 transitions of a TLA+
model of a FIFO, as distributed with the
@@ -74,7 +75,7 @@ using the "Custom Transition Diagram" feature of ProB:
image::MCInnerFIFO_proj_cardq.png[]
[[rushhour]]
-=== RushHour
+== RushHour
This is a visualisation of the
<<rush-hour-puzzle, Rush
@@ -90,7 +91,7 @@ transitions, using the scale option this time:
image::RushHour_full_sfdp.png[]
[[can-bus]]
-=== CAN Bus
+== CAN Bus
This is a visualisation of the statespace of an Event-B model of a CAN
Bus. The colours indicate the size of the BUSwrite variable
@@ -99,7 +100,7 @@ Bus. The colours indicate the size of the BUSwrite variable
image::CANBus_sfdp.png[]
[[hanoi-6-discs]]
-=== Hanoi (6 Discs)
+== Hanoi (6 Discs)
This is a visualisation of the statespace of a B model of the towers of
Hanoi for 6 discs. The state space contains 731 nodes and 2186 nodes.
@@ -117,7 +118,7 @@ ProB:
image::Hanoi6_proj_cardondest.png[]
[[threads---partial-order-reduction]]
-=== Threads - Partial Order Reduction
+== Threads - Partial Order Reduction
This is the visualisation of a simple threads model, of two threads with
n=51 steps before a synchronisation occurs and threads start again. The
diff --git a/src/docs/chapter/user/22_Visualisation/30_Eval_Console.adoc b/src/docs/chapter/user/22_Visualisation/30_Eval_Console.adoc
index 6123320..cd659b9 100644
--- a/src/docs/chapter/user/22_Visualisation/30_Eval_Console.adoc
+++ b/src/docs/chapter/user/22_Visualisation/30_Eval_Console.adoc
@@ -1,5 +1,6 @@
+
[[eval-console]]
-== Eval Console
+= Eval Console
For this tutorial, load for example the file `StackConstructive.mch`
included in the `examples/Tutorial` directory of the
diff --git a/src/docs/chapter/user/22_Visualisation/31_Evaluation_View.adoc b/src/docs/chapter/user/22_Visualisation/31_Evaluation_View.adoc
index 155be09..4db415e 100644
--- a/src/docs/chapter/user/22_Visualisation/31_Evaluation_View.adoc
+++ b/src/docs/chapter/user/22_Visualisation/31_Evaluation_View.adoc
@@ -1,5 +1,6 @@
+
[[evaluation-view]]
-== Evaluation View
+= Evaluation View
This tutorial describes the use of ProB's evaluation view to
explore single states of a model. The view shows the details of a
@@ -15,7 +16,7 @@ the values of the sub-expressions.
ProB.
[[inspecting-the-state-variables-and-constants]]
-=== Inspecting the State Variables and Constants
+== Inspecting the State Variables and Constants
As an example specification we use the Sieve.mch delivered with the ProB
Distribution in the "Less Simple" folder. After opening the model do a
@@ -44,7 +45,7 @@ B-Expression) to a file. You can also save the values of multiple
variables (we will cover this later).
[[understanding-the-invariant-and-properties]]
-=== Understanding the Invariant and Properties
+== Understanding the Invariant and Properties
The second objective of the evaluation view is to help understanding why
the invariant or the properties are true or false. Therefore the view
@@ -124,7 +125,7 @@ introduced predicate it is very easy to see the reason why
image::Eval_view6.png[]
[[filtering-relevant-information-and-data-extraction]]
-=== Filtering relevant information and Data Extraction
+== Filtering relevant information and Data Extraction
There are two different ways to filter out important information from a
state. To demonstrate this feature we can use the model
diff --git a/src/docs/chapter/user/22_Visualisation/40_Graphical_Visualization.adoc b/src/docs/chapter/user/22_Visualisation/40_Graphical_Visualization.adoc
index ae128cd..47cc70e 100644
--- a/src/docs/chapter/user/22_Visualisation/40_Graphical_Visualization.adoc
+++ b/src/docs/chapter/user/22_Visualisation/40_Graphical_Visualization.adoc
@@ -1,5 +1,6 @@
+
[[graphical-visualization]]
-== Graphical Visualization
+= Graphical Visualization
The graphical visualization of ProB footnote:[M. Leuschel, M. Samia, J. Bendisposto
and L. Luo: Easy Graphical Animation and Formula Viewing for Teaching B.
@@ -14,7 +15,7 @@ function in B stipulates which pictures should be displayed. We now show
how this animation can be done with very little effort.
[[the-graphical-animation-model]]
-=== The Graphical Animation Model
+== The Graphical Animation Model
The animation model is very simple. It is based on individual images and
a user-defined animation function, which are both defined in the
@@ -156,13 +157,13 @@ can directly handle user sets but does not work well if we need a
special image for undefined,...)
[[further-examples]]
-=== Further Examples
+== Further Examples
Below we illustrate how the graphical animation model easily provides
interesting animations for different models.
[[scheduler]]
-==== Scheduler
+=== Scheduler
The scheduler specification taken from footnote:[B. Legeard, F. Peureux,
and M. Utting. Automated boundary testing from Z and B. Proceedings of
@@ -245,7 +246,7 @@ ANIMATION_FUNCTION == ({r,c,i| r=1 & i:PID & c=i & i:waiting} \/
----
[[sudoku]]
-==== Sudoku
+=== Sudoku
Using ProB we can also solve Sudoku puzzles. The machine has the
variable Sudoku9 of type `1..fullsize-->(1..fullsize+->NRS)`, where NRS is
@@ -293,7 +294,7 @@ c:dom(Sudoku9(r)) & i:1.. fullsize & i = Sudoku9(r)(c)}
)
----
-=== Other Features
+== Other Features
One can define actions for right clicks and mouse clicks and drags:
----
@@ -321,7 +322,7 @@ The following preferences can be used to control padding around cells:
SET_PREF_TK_CUSTOM_STATE_VIEW_STRING_PADDING == Nr
SET_PREF_TK_CUSTOM_STATE_VIEW_PADDING == Nr
-----
-
+
The following preference can be used to disable the custom graphical visualization view:
-----
SET_PREF_TK_CUSTOM_STATE_VIEW_VISIBLE == FALSE
@@ -332,4 +333,3 @@ One can control justification of animation strings using either of the two follo
ANIMATION_STR_JUSTIFY_LEFT == TRUE
ANIMATION_STR_JUSTIFY_RIGHT == TRUE
-----
-
diff --git a/src/docs/chapter/user/22_Visualisation/ZZ_section_footer.adoc b/src/docs/chapter/user/22_Visualisation/ZZ_section_footer.adoc
new file mode 100644
index 0000000..909c09e
--- /dev/null
+++ b/src/docs/chapter/user/22_Visualisation/ZZ_section_footer.adoc
@@ -0,0 +1,2 @@
+
+:leveloffset: -1
diff --git a/src/docs/chapter/user/25_CommandLine/00_CommandLine.adoc b/src/docs/chapter/user/25_CommandLine/00_section_header.adoc
similarity index 64%
rename from src/docs/chapter/user/25_CommandLine/00_CommandLine.adoc
rename to src/docs/chapter/user/25_CommandLine/00_section_header.adoc
index df5315f..9b893ce 100644
--- a/src/docs/chapter/user/25_CommandLine/00_CommandLine.adoc
+++ b/src/docs/chapter/user/25_CommandLine/00_section_header.adoc
@@ -1,2 +1,4 @@
+
[[command-line]]
= Command Line
+:leveloffset: +1
diff --git a/src/docs/chapter/user/25_CommandLine/01_ProB_Cli.adoc b/src/docs/chapter/user/25_CommandLine/01_ProB_Cli.adoc
index 4924a74..7a9e483 100644
--- a/src/docs/chapter/user/25_CommandLine/01_ProB_Cli.adoc
+++ b/src/docs/chapter/user/25_CommandLine/01_ProB_Cli.adoc
@@ -1,6 +1,6 @@
[[prob-cli]]
-== ProB CLI
+= ProB CLI
The ProB Cli (command-line interface) offers many of the ProB features
via command-line. As such, you can run ProB from your shell scripts or
diff --git a/src/docs/chapter/user/25_CommandLine/02_Using_the_Command-Line_Version_of_ProB.adoc b/src/docs/chapter/user/25_CommandLine/02_Using_the_Command-Line_Version_of_ProB.adoc
index 7310f26..e550cd8 100644
--- a/src/docs/chapter/user/25_CommandLine/02_Using_the_Command-Line_Version_of_ProB.adoc
+++ b/src/docs/chapter/user/25_CommandLine/02_Using_the_Command-Line_Version_of_ProB.adoc
@@ -1,5 +1,6 @@
+
[[using-the-command-line-version-of-prob]]
-== Using the Command-Line Version of ProB
+= Using the Command-Line Version of ProB
The command-line version of ProB, called probcli, offers many of the
features of the standalone Tcl/Tk Version via the command-line. As such,
@@ -14,7 +15,7 @@ groups of commands such as `-p MAXINT 127`). Any argument that is not
recognised by `probcli` is treated as a filename to be analysed.
[[conventions-used]]
-=== Conventions used
+== Conventions used
The following conventions are used in this guide:
@@ -25,7 +26,7 @@ The following conventions are used in this guide:
|=======================================================================
[[synopsis]]
-=== Synopsis
+== Synopsis
....
|probcli [--help]
@@ -45,19 +46,19 @@ probcli M.mch --model-check
....
[[options-for-command-line]]
-=== Options
+== Options
[[mc]]
-==== -mc
+=== -mc
-===== Description
+==== Description
[cols="",]
|====================================
|model check; checking at most <nr> states
|====================================
-===== Example
+==== Example
....
probcli my.mch -mc 100
@@ -71,15 +72,15 @@ using the `-goal "PRED"` command and limit the scope of the model
checking using the `-scope "PRED"` command.
[[model_check]]
-==== -model_check
+=== -model_check
The same as `-mc` but without a limit on the number of nodes checked.
ProB will run until the entire state space is explored.
[[no]]
-==== -no <x>
+=== -no <x>
-===== Description
+==== Description
[cols="",]
|=======================================================================
@@ -91,16 +92,16 @@ ProB will run until the entire state space is explored.
* `-nogoal` : do not stop if a state satisfying the GOAL predicate has been found
* `-noass` : do not report assertion violations
-===== Example
+==== Example
....
probcli my.mch -mc 1000 -nodead -nogoal
....
[[disable_timeout]]
-==== -disable_timeout
+=== -disable_timeout
-===== Description
+==== Description
[cols="",]
|=======================================================================
@@ -110,48 +111,48 @@ checking (-mc or -model_check) and animation (-animate). Available as of
version 1.5.1-beta7.
|=======================================================================
-===== Example
+==== Example
....
probcli my.mch -model-check -disable-timeout
....
[[bf]]
-==== -bf
+=== -bf
-===== Description
+==== Description
[cols="",]
|===========================================
|proceed breadth-first during model checking
|===========================================
-===== Example
+==== Example
....
probcli my.mch -bf -mc 1000
....
[[df]]
-==== -df
+=== -df
-===== Description
+==== Description
[cols="",]
|=========================================
|proceed depth-first during model checking
|=========================================
-===== Example
+==== Example
....
probcli my.mch -df -mc 1000
....
[[mc_mode]]
-==== -mc_mode <M>
+=== -mc_mode <M>
-===== Description
+==== Description
[cols="",]
|=======================================================================
@@ -175,16 +176,16 @@ directed model checking>>.
* `out_degree_hash` (prioritise nodes with fewer outgoing transitions;
mainly useful for deadlock checking)
-===== Example
+==== Example
....
probcli my.mch -model_check -mc_mode random
....
[[timeout]]
-==== --timeout <N>
+=== --timeout <N>
-===== Description
+==== Description
[cols="",]
|=======================================================================
@@ -196,39 +197,39 @@ as invariant checking or static assertion checking, where it is
multiplied by a factor. See the description of the -p option.
|=======================================================================
-===== Example
+==== Example
....
probcli my.mch -timeout 10000
....
[[t]]
-==== -t
+=== -t
-===== Description
+==== Description
[cols="",]
|===============================================
|trace check (associated .trace file must exist)
|===============================================
-===== Example
+==== Example
....
probcli my.mch -t
....
[[init]]
-==== -init
+=== -init
-===== Description
+==== Description
[cols="",]
|========================
|initialise specification
|========================
-===== Example
+==== Example
....
probcli my.mch -init
@@ -255,25 +256,25 @@ ALL OPERATIONS COVERED
....
[[cbc]]
-==== -cbc <OPNAME>
+=== -cbc <OPNAME>
-===== Description
+==== Description
[cols="",]
|====================================================================
|constraint-based invariant checking for an operation (also use <OPNAME>=all)
|====================================================================
-===== Example
+==== Example
....
probcli my.mch -cbc all
....
[[cbc_deadlock]]
-==== -cbc_deadlock
+=== -cbc_deadlock
-===== Description
+==== Description
[cols="",]
|=======================================================================
@@ -288,9 +289,9 @@ state(s). If you want to find a reachable deadlock you have to use the
model checker.
[[cbc_deadlock_pred]]
-==== -cbc_deadlock_pred <PRED>
+=== -cbc_deadlock_pred <PRED>
-===== Description
+==== Description
[cols="",]
|===================================================
@@ -300,16 +301,16 @@ model checker.
This is like -cbc_deadlock but you provide an additional predicate. ProB
will only find deadlocks which also make this predicate true.
-===== Example
+==== Example
....
probcli my.mch -cbc_deadlock_pred "n=15"
....
[[cbc_assertions]]
-==== -cbc_assertions
+=== -cbc_assertions
-===== Description
+==== Description
[cols="",]
|====================================================
@@ -341,9 +342,9 @@ ASSERTION(s) are tautologies. Both commands can be useful to use ProB as
a Prover/Disprover (as is done in Atelier-B 4.3).
[[cbc_sequence]]
-==== -cbc_sequence <SEQ>
+=== -cbc_sequence <SEQ>
-===== Description
+==== Description
[cols="",]
|=======================================================================
@@ -354,16 +355,16 @@ This will try to find a solution for the constants, initial variable
values and parameters which make execution of the given sequence of
operations possible.
-===== Example
+==== Example
....
probcli my.mch -cbc_sequence "op1;op2"
....
[[strict]]
-==== -strict
+=== -strict
-===== Description
+==== Description
[cols="",]
|=======================================================================
@@ -372,16 +373,16 @@ model checking finds a counter example or trace checking fails or any
unexpected error happens
|=======================================================================
-===== Example
+==== Example
....
probcli my.mch -t -strict
....
[[expcterr]]
-==== -expcterr <ERR>
+=== -expcterr <ERR>
-===== Description
+==== Description
[cols="",]
|=======================================================================
@@ -390,16 +391,16 @@ certain error to occur. Mainly useful for regression tests (in
conjunction with the -strict option).
|=======================================================================
-===== Example
+==== Example
....
probcli examples/B/Benchmarks/CarlaTravelAgencyErr.mch -mc 1000 -expcterr invariant_violation -strict
....
[[animate]]
-==== -animate <Nr>
+=== -animate <Nr>
-===== Description
+==== Description
[cols="",]
|===============================
@@ -411,16 +412,16 @@ deadlock is reached and report an error. You can also use the command
`-animate_all`, which will only stop at a deadlock (and not report an
error). Be careful: `-animate_all` could run forever.
-===== Example
+==== Example
....
probcli my.mch -animate 100
....
[[execute]]
-==== -execute <Nr>
+=== -execute <Nr>
-===== Description
+==== Description
[cols="",]
|========================
@@ -444,16 +445,16 @@ operations in the B machine is thus important for -execute
faster but after execution one only has access to the first state and
the final state of execution
-===== Example
+==== Example
....
probcli my.mch -execute 100
....
[[det_check]]
-==== -det_check
+=== -det_check
-===== Description
+==== Description
[cols="",]
|==========================================
@@ -465,16 +466,16 @@ operation is possible, and it can only be executed in one possible way
as far as parameters and result is concerned). Currently this option has
only an effect for the -animate and the -init commands.
-===== Example
+==== Example
....
probcli my.mch -animate 100 -det_check
....
[[det_constants]]
-==== -det_constants
+=== -det_constants
-===== Description
+==== Description
[cols="",]
|==========================================
@@ -485,16 +486,16 @@ Checks if the SETUP_CONSTANTS step is deterministic (i.e., only one way
to set up the constants is possible). Currently this option has only an
effect for the -animate and the -init commands.
-===== Example
+==== Example
....
probcli my.mch -init -det_constants
....
[[his]]
-==== -his <FILE>
+=== -his <FILE>
-===== Description
+==== Description
[cols="",]
|================================
@@ -510,7 +511,7 @@ initial state is written out. The -his command is executed after the
-init, -animate, -t or -mc commands. See also the -sptxt command to only
write the current values of variables and constants to a file.
-===== Example
+==== Example
....
probcli -animate 5 -his history.txt supersimple.mch
@@ -533,9 +534,9 @@ With -his_option trace_file as only option, probcli will write the
history in Prolog format, which can later be used by the -t command.
[[i]]
-==== -i
+=== -i
-===== Description
+==== Description
[cols="",]
|=====================
@@ -545,23 +546,23 @@ history in Prolog format, which can later be used by the -t command.
After performing the other commands, ProB stays in interactive mode and
allows the user to manually animate the loaded specification.
-===== Example
+==== Example
....
probcli my.mch -i
....
[[repl]]
-==== -repl
+=== -repl
-===== Description
+==== Description
[cols="",]
|======================================
|start interactive read-eval-print-loop
|======================================
-===== Example
+==== Example
....
probcli my.mch -p CLPFD TRUE -repl
@@ -592,16 +593,16 @@ probcli -eval_file MyFormula.txt
....
[[c]]
-==== -c
+=== -c
-===== Description
+==== Description
[cols="",]
|=========================
|print coverage statistics
|=========================
-===== Example
+==== Example
....
probcli my.mch -mc 1000 -c
@@ -621,9 +622,9 @@ probcli my.mch -mc 1000 --coverage_summary
....
[[cc]]
-==== -cc <Nr> <Nr>
+=== -cc <Nr> <Nr>
-===== Description
+==== Description
[cols="",]
|=======================================================================
@@ -631,16 +632,16 @@ probcli my.mch -mc 1000 --coverage_summary
that the given number of nodes and transitions have been computed.
|=======================================================================
-===== Example
+==== Example
....
probcli my.mch -mc 1000 -cc 10 25
....
[[p]]
-==== -p <PREFERENCE> <VALUE>
+=== -p <PREFERENCE> <VALUE>
-===== Description
+==== Description
[cols="",]
|=======================================================================
@@ -650,7 +651,7 @@ probcli my.mch -mc 1000 -cc 10 25
You can also use --pref instead of -p.
-===== Example
+==== Example
....
probcli my.mch -p TIME_OUT 8000 -p CLPFD TRUE -mc 10000
@@ -658,9 +659,9 @@ probcli my.mch -p TIME_OUT 8000 -p CLPFD TRUE -mc 10000
[[prefs]]
-==== -pref_group <PREFGROUP> <SETTING>
+=== -pref_group <PREFGROUP> <SETTING>
-===== Description
+==== Description
[cols="",]
|=======================================================================
@@ -668,7 +669,7 @@ probcli my.mch -p TIME_OUT 8000 -p CLPFD TRUE -mc 10000
|=======================================================================
-===== Example
+==== Example
....
probcli my.mch -pref_group model_check unlimited
@@ -680,9 +681,9 @@ Available groups and settings are:
- PREFERENCE GROUP model_check : SETTINGS [disable_max,unlimited] : Model Checking Limits
- PREFERENCE GROUP dot_colors : SETTINGS [classic,dreams,winter] : Colours for Dot graphs
-==== -prefs <FILE>
+=== -prefs <FILE>
-===== Description
+==== Description
[cols="",]
|=======================================================================
@@ -693,16 +694,16 @@ please have a look at
<<using-the-command-line-version-of-prob,Preferences>>
|=======================================================================
-===== Example
+==== Example
....
probcli my.mch -prefs ProB_Preferences.pl
....
[[card]]
-==== -card <GS> <VAL>
+=== -card <GS> <VAL>
-===== Description
+==== Description
[cols="",]
|=======================================================================
@@ -711,32 +712,32 @@ overrides the default cardinality (which can be set using
`-p DEFAULT_SETSIZE`).
|=======================================================================
-===== Example
+==== Example
....
probcli my.mch -card PID 5
....
[[goal]]
-==== -goal <PRED>
+=== -goal <PRED>
-===== Description
+==== Description
[cols="",]
|====================================
|set GOAL predicate for model checker
|====================================
-===== Example
+==== Example
....
probcli my.mch -mc 10000000 -goal "n=18"-strict -expcterr goal_found
....
[[scope]]
-==== -scope <PRED>
+=== -scope <PRED>
-===== Description
+==== Description
[cols="",]
|=======================================================================
@@ -745,64 +746,64 @@ SCOPE predicate will be ignored (invariant will not be checked and no
outgoing transitions will be computed)
|=======================================================================
-===== Example
+==== Example
....
probcli my.mch -mc 10000000 -scope "n<18"
....
[[s]]
-==== -s <PORT>
+=== -s <PORT>
-===== Description
+==== Description
[cols="",]
|=================================
|start socket server on given port
|=================================
-===== Example
+==== Example
....
probcli my.mch ...
....
[[ss]]
-==== -ss
+=== -ss
-===== Description
+==== Description
[cols="",]
|================================
|start socket server on port 9000
|================================
-===== Example
+==== Example
....
probcli my.mch ...
....
[[sf]]
-==== -sf
+=== -sf
-===== Description
+==== Description
[cols="",]
|=====================================
|start socket server on some free port
|=====================================
-===== Example
+==== Example
....
probcli my.mch ...
....
[[sptxt]]
-==== -sptxt <FILE>
+=== -sptxt <FILE>
-===== Description
+==== Description
[cols="",]
|======================================
@@ -816,7 +817,7 @@ infinite sets may be written out symbolically).
See also the -his command.
-===== Example
+==== Example
....
probcli -animate 5 -sptxt state.txt supersimple.mch
@@ -826,9 +827,9 @@ This will write the values of all variables and constants to the file
state.txt after animating the machine 5 steps.
[[cache]]
-==== -cache <DIRECTORY>
+=== -cache <DIRECTORY>
-===== Description
+==== Description
[cols="",]
|=======================================================================
@@ -848,25 +849,25 @@ However, we do not support refinements at the moment.
NOTE: this command can also be used when starting up the ProB Tcl/Tk version.
[[logxml]]
-==== -logxml <LogFile>
+=== -logxml <LogFile>
-===== Description
+==== Description
[cols="",]
|======================================================
|log activities and results of probcli in XML format in <LogFile>
|======================================================
-===== Example
+==== Example
....
probcli my.mch -mc 1000 -logxml log.xml
....
[[logxml_write_vars]]
-==== -logxml_write_vars <PREFIX>
+=== -logxml_write_vars <PREFIX>
-===== Description
+==== Description
[cols="",]
|=======================================================================
@@ -875,80 +876,80 @@ variables having prefix PREFIX in their name into the XML log file (if
XML logging has been activated using the -logxml command)
|=======================================================================
-===== Example
+==== Example
....
probcli my.mch -execute 1000 -logxml log.xml -logxml_write_vars out
....
[[l]]
-==== -l <LogFile>
+=== -l <LogFile>
-===== Description
+==== Description
[cols="",]
|=====================================
|log activities <LogFile> in using Prolog format
|=====================================
-===== Example
+==== Example
....
probcli my.mch -mc 1000 -l my.log
....
[[ll]]
-==== -ll
+=== -ll
-===== Description
+==== Description
[cols="",]
|=========================================
|log activities in /tmp/prob_cli_debug.log
|=========================================
-===== Example
+==== Example
....
probcli my.mch -mc 1000 -ll
....
[[lg]]
-==== -lg <LogFile>
+=== -lg <LogFile>
-===== Description
+==== Description
[cols="",]
|=====================
|analyse <LogFile> using gnuplot
|=====================
-===== Example
+==== Example
....
probcli my.mch ...
....
[[pp]]
-==== -pp <FILE>
+=== -pp <FILE>
-===== Description
+==== Description
[cols="",]
|=======================================
|pretty-print internal representation to <FILE>
|=======================================
-===== Example
+==== Example
....
probcli my.mch -pp my_pp.mch
....
[[ppf]]
-==== -ppf <FILE>
+=== -ppf <FILE>
-===== Description
+==== Description
[cols="",]
|=======================================================================
@@ -956,32 +957,32 @@ probcli my.mch -pp my_pp.mch
infos
|=======================================================================
-===== Example
+==== Example
....
probcli my.mch -ppf my_ppf.mch
....
[[v]]
-==== -v
+=== -v
-===== Description
+==== Description
[cols="",]
|==========================
|set ProB into verbose mode
|==========================
-===== Example
+==== Example
....
probcli my.mch -mc 1000 -v
....
[[version]]
-==== -version
+=== -version
-===== Description
+==== Description
[cols="",]
|=========================
@@ -991,7 +992,7 @@ probcli my.mch -mc 1000 -v
There is also an alternate command called -svers which just prints the
version number of ProB.
-===== Example
+==== Example
....
probcli -version
@@ -1011,9 +1012,9 @@ You can use `probcli -version -v` to obtain more information about your
version of probcli.
[[check_java_version]]
-==== -check_java_version
+=== -check_java_version
-===== Description
+==== Description
[cols="",]
|===========================================
@@ -1032,9 +1033,9 @@ Result of checking Java version:
....
[[assertions]]
-==== -assertions
+=== -assertions
-===== Description
+==== Description
[cols="",]
|===================================
@@ -1055,16 +1056,16 @@ machine which are not linked (directly or indirectly) to the ASSERTIONS.
This optimization will only be made if you provide no other switch, such
as -mc or -animate which may require the computation of the variables.
-===== Example
+==== Example
....
probcli my.mch -init -assertions
....
[[properties]]
-==== -properties
+=== -properties
-===== Description
+==== Description
[cols="",]
|=======================================================================
@@ -1073,16 +1074,16 @@ probcli my.mch -init -assertions
will debug the properties.
|=======================================================================
-===== Example
+==== Example
....
probcli my.mch -init -properties
....
[[dot_output]]
-==== -dot_output <PATH>
+=== -dot_output <PATH>
-===== Description
+==== Description
[cols="",]
|=======================================================================
@@ -1096,7 +1097,7 @@ property or assertion. Assertions are numbered A0,A1,... and properties
P0,P1,... You can also force to generate dot files for all properties
(i.e., also the true ones) using the -dot_all command-line flag.
-===== Example
+==== Example
....
probcli my.mch -init -properties -dot_output somewhere/
@@ -1106,103 +1107,103 @@ This will generate files somewhere/my_P0_false.dot,
somewhere/my_P1_false.dot, ...
[[rc]]
-==== -rc
+=== -rc
-===== Description
+==== Description
[cols="",]
|==============================================
|runtime checking of types/pre-/post-conditions
|==============================================
-===== Example
+==== Example
....
probcli my.mch ...
....
[[ltlfile]]
-==== -ltlfile <FILE>
+=== -ltlfile <FILE>
-===== Description
+==== Description
[cols="",]
|==========================
|check LTL formulas in file <FILE>
|==========================
-===== Example
+==== Example
....
probcli my.mch ...
....
[[ltlassertions]]
-==== -ltlassertions
+=== -ltlassertions
-===== Description
+==== Description
[cols="",]
|=====================================
|check LTL assertions (in DEFINITIONS)
|=====================================
-===== Example
+==== Example
....
probcli my.mch ...
....
[[ltllimit]]
-==== -ltllimit <LIMIT>
+=== -ltllimit <LIMIT>
-===== Description
+==== Description
[cols="",]
|==============================================
|explore at most <LIMIT> states when model-checking LTL
|==============================================
-===== Example
+==== Example
....
probcli my.mch ...
....
[[save]]
-==== -save <FILE>
+=== -save <FILE>
-===== Description
+==== Description
[cols="",]
|===========================================
|save state space for later refinement check
|===========================================
-===== Example
+==== Example
....
probcli my.mch ...
....
[[refchk]]
-==== -refchk <FILE>
+=== -refchk <FILE>
-===== Description
+==== Description
[cols="",]
|===================================================
|refinement check against previous saved state space
|===================================================
-===== Example
+==== Example
....
probcli my.mch ...
....
[[mcm_tests]]
-==== -mcm_tests <Depth> <MaxStates> <EndPredicate> <FILE>
+=== -mcm_tests <Depth> <MaxStates> <EndPredicate> <FILE>
Generate test cases for the given specification. Each test case consists
of a sequence of operations resp. events (a so-called trace) that
@@ -1242,7 +1243,7 @@ EndPredicate::
FILE::
The found test cases a written to the XML file .
-===== Example
+==== Example
....
probcli my.mch -mcm_tests 10 2000 EndStateVar=TRUE testcases.xml -mcm_cover op1,op2
@@ -1265,7 +1266,7 @@ exists are written into the trace file, as argument of an INITIALISATION
event.
[[mcm_cover]]
-==== -mcm_cover <Operation(s)>
+=== -mcm_cover <Operation(s)>
Specify an operation or event that should be covered when generating
test cases with the *-mcm_test* option. Multiple operations/events can
@@ -1275,23 +1276,23 @@ several times.
See <<mcm-tests, -mcm-tests>> for further details.
[[spdot]]
-==== -spdot <FILE>
+=== -spdot <FILE>
-===== Description
+==== Description
[cols="",]
|=======================================
|Write graph of the state space to a dot <FILE>
|=======================================
-===== Example
+==== Example
....
probcli my.mch -mc 100 -spdot my_statespace.dot
....
[[cbc_tests]]
-==== -cbc_tests <Depth> <EndPredicate> <File>
+=== -cbc_tests <Depth> <EndPredicate> <File>
Generate test cases by constraint solving with maximum length *Depth*,
the last state satisfies *EndPredicate* and the test cases are written
@@ -1300,7 +1301,7 @@ filename is the empty string no file is generated. See also the page on
<<test-case-generation,Test_Case_Generation>>.
[[cbc_cover]]
-==== -cbc_cover <Operation>
+=== -cbc_cover <Operation>
When generating CB test cases, *Operation* should be covered.
The option can be given multiple times to specify several operations.
@@ -1315,12 +1316,12 @@ to match all operations whose name contains PartialName. See also the
page about <<test-case-generation,Test_Case_Generation>>.
[[test_description]]
-==== -test_description <File>
+=== -test_description <File>
Read the options for constraint based test case generation from *File*.
[[bmc]]
-==== -bmc <Depth>
+=== -bmc <Depth>
[cols="",]
|=======================================================================
@@ -1329,27 +1330,27 @@ maximum trace depth specified. Looks for invariant violations using the
constraint-based test case generation algorithm.
|=======================================================================
-===== Example
+==== Example
....
probcli my.mch -bmc 20
....
[[csp-guide]]
-==== -csp-guide <File>
+=== -csp-guide <File>
Use the CSP File *File* to guide the B Machine ("CSP||B"). (This
feature is included since version 1.3.5-beta7.)
[[environment-variables-for-command-line]]
-=== Environment Variables
+== Environment Variables
Set NO_COLOR environment variable to disable terminal colors.
See also https://no-color.org[https://no-color.org].
[[preferences-for-command-line]]
-=== Preferences
+== Preferences
You can use these preferences within the command:
@@ -1478,14 +1479,14 @@ in conjunction with Ignore Hash Collisions)
B substitutions
|=======================================================================
-==== Example
+=== Example
....
probcli my.mch -p TIME_OUT 5000 -p CLPFD TRUE -p SYMMETRY_MODE hash -mc 1000
....
[[some-probcli-examples]]
-=== Some probcli examples
+== Some probcli examples
To load a file My.mch, setup the constants and initialize it do:
@@ -1517,7 +1518,7 @@ probcli -p COMPRESSION -p IGNORE_HASH_COLLISIONS TRUE -p FORGET_STATE_SPACE TRUE
....
[[command-line-arguments-for-prob-tcltk]]
-=== Command-line Arguments for ProB Tcl/Tk
+== Command-line Arguments for ProB Tcl/Tk
Note that the stand-alone Tcl/Tk version also supports a limited form of
command-line preferences:
diff --git a/src/docs/chapter/user/25_CommandLine/ZZ_section_footer.adoc b/src/docs/chapter/user/25_CommandLine/ZZ_section_footer.adoc
new file mode 100644
index 0000000..909c09e
--- /dev/null
+++ b/src/docs/chapter/user/25_CommandLine/ZZ_section_footer.adoc
@@ -0,0 +1,2 @@
+
+:leveloffset: -1
diff --git a/src/docs/chapter/user/30_OtherLanguages/00_section_header.adoc b/src/docs/chapter/user/30_OtherLanguages/00_section_header.adoc
new file mode 100644
index 0000000..b6c828a
--- /dev/null
+++ b/src/docs/chapter/user/30_OtherLanguages/00_section_header.adoc
@@ -0,0 +1,4 @@
+
+[[other-languages]]
+= Other languages
+:leveloffset: +1
diff --git a/src/docs/chapter/user/30_OtherLanguages/00_Other_languages.adoc b/src/docs/chapter/user/30_OtherLanguages/01_Other_languages.adoc
similarity index 98%
rename from src/docs/chapter/user/30_OtherLanguages/00_Other_languages.adoc
rename to src/docs/chapter/user/30_OtherLanguages/01_Other_languages.adoc
index 7db97cc..21cab28 100644
--- a/src/docs/chapter/user/30_OtherLanguages/00_Other_languages.adoc
+++ b/src/docs/chapter/user/30_OtherLanguages/01_Other_languages.adoc
@@ -1,5 +1,6 @@
-[[other-languages]]
-= Other languages
+
+[[other-languages-overview]]
+= Overview
Since version
1.2.7 of ProB (July 2008) you can also open Promela files with ProB.
@@ -96,7 +97,7 @@ the Rush Hour puzzle>> which also includes a graphical visualisation
(using the `animation_function_result` predicate recognised by ProB as
of version 1.4.0-rc3).
-== Other recognised Prolog predicates
+= Other recognised Prolog predicates
The following can be used to set up an animation image matrix with corresponding actions:
* animation_image(Nr,Path)
diff --git a/src/docs/chapter/user/30_OtherLanguages/Alloy.adoc b/src/docs/chapter/user/30_OtherLanguages/Alloy.adoc
index f9844bb..2db78e1 100644
--- a/src/docs/chapter/user/30_OtherLanguages/Alloy.adoc
+++ b/src/docs/chapter/user/30_OtherLanguages/Alloy.adoc
@@ -1,5 +1,6 @@
+
[[alloy]]
-== Alloy
+= Alloy
As of version 1.8 ProB provides support to load
http://alloy.mit.edu/alloy/[Alloy] models. The Alloy models are
@@ -17,7 +18,7 @@ B language. In addition to basic Alloy constructs, our approach supports
integers and orderings.
[[installation-alloy]]
-=== Installation
+== Installation
Alloy2B is included as of version 1.8.2 of ProB.
@@ -29,10 +30,10 @@ on Github].
* put resulting alloy2b-*.jar file into ProB's lib folder.
[[examples-alloy]]
-=== Examples
+== Examples
[[n-queens-alloy]]
-==== N-Queens
+=== N-Queens
....
module queens
@@ -79,7 +80,7 @@ PROPERTIES
x : queen --> INTEGER
& x_ : queen --> INTEGER
& y : queen --> INTEGER
- & !this.(this : queen => x(this) >= 1 & y(this) >= 1 & x(this) <= card(queen) & y(this) <=
+ & !this.(this : queen => x(this) >= 1 & y(this) >= 1 & x(this) <= card(queen) & y(this) <=
card(queen) & x_(this) >= 1 & x_(this) <= card(queen) & x_(this) = (card(queen) + 1) - x(this)
)
& card(queen) = 4
@@ -88,8 +89,8 @@ PROPERTIES
INITIALISATION
skip
OPERATIONS
- run0 =
- PRE
+ run0 =
+ PRE
card(queen) = 4
& !(q,q_).(q_ : queen - {q} => not(x(q) = x(q_)) & not(y(q) = y(q_)) & not(x(q) + y(q)
= x(q_) + y(q_)) & not(x_(q) + y(q) = x_(q_) + y(q_)))
@@ -103,7 +104,7 @@ END
[[river-crossing-puzzle]]
-==== River Crossing Puzzle
+=== River Crossing Puzzle
....
module river_crossing
open util/ordering[State]
@@ -186,7 +187,7 @@ END
....
[[proof-with-atelier-b-example]]
-==== Proof with Atelier-B Example
+=== Proof with Atelier-B Example
....
sig Object {}
@@ -243,7 +244,7 @@ image::AlloyAtelierB.png[]
[[Alloy-Syntax]]
-==== Alloy Syntax
+=== Alloy Syntax
....
Logical predicates:
-------------------
@@ -266,8 +267,8 @@ Quantifiers:
some DECL | P existential quantification
one DECL | P existential quantification with exactly one solution
lone DECL | P quantification with one or zero solutions
-
-where the DECL follow the following form:
+
+where the DECL follow the following form:
x : S choose a singleton subset of S (like x : one S)
x : one S choose a singleton subset of S
x : S choose x to be any subset of S
@@ -309,7 +310,7 @@ Relation Expressions:
~R relational inverse
^R transitive closure of binary relation
*R reflexive and transitive closure
-
+
Multiplicity Declarations:
---------------------------
The following multiplicity annotations are supported for binary (sub)-relations:
@@ -345,7 +346,7 @@ A signature S can be defined to be ordered:
s/lte[s2] true if index(e1) =< index(e2)
s/gt[s2] true if index(e1) > index(e2)
s/gte[s2] true if index(e1) >= index(e2)
-
+
Sequences:
----------
The longest allowed sequence length (maxseq) is set in the scope of a run or check command using the 'seq' keyword.
diff --git a/src/docs/chapter/developer/30_tcltk/00_section_header.adoc b/src/docs/chapter/user/30_OtherLanguages/CSP/00_section_header.adoc
similarity index 53%
rename from src/docs/chapter/developer/30_tcltk/00_section_header.adoc
rename to src/docs/chapter/user/30_OtherLanguages/CSP/00_section_header.adoc
index ef81078..e0d3ed9 100644
--- a/src/docs/chapter/developer/30_tcltk/00_section_header.adoc
+++ b/src/docs/chapter/user/30_OtherLanguages/CSP/00_section_header.adoc
@@ -1,2 +1,4 @@
-= Prolog
+
+[[csp]]
+= CSP
:leveloffset: +1
diff --git a/src/docs/chapter/user/30_OtherLanguages/CSP/01_CSP-M.adoc b/src/docs/chapter/user/30_OtherLanguages/CSP/01_CSP-M.adoc
index bf7ef7d..58c9a83 100644
--- a/src/docs/chapter/user/30_OtherLanguages/CSP/01_CSP-M.adoc
+++ b/src/docs/chapter/user/30_OtherLanguages/CSP/01_CSP-M.adoc
@@ -1,8 +1,6 @@
-[[csp]]
-== CSP
[[csp-m]]
-=== CSP-M
+= CSP-M
ProB supports
machine readable CSPfootnote:[M. Butler and M. Leuschel: _Combining CSP
@@ -21,7 +19,7 @@ below)
current B machine to control it
[[limitations-of-csp-m-support]]
-==== Limitations of CSP-M Support
+== Limitations of CSP-M Support
ProB now supports FDR and ProBE compatible CSP-M syntax, with the
following outstanding issues
@@ -50,7 +48,7 @@ We still need to tune the animator and model checker for efficiency
deeply nested CSP synchronization constructs).
[[guiding-b-machines-with-csp]]
-==== Guiding B Machines with CSP
+== Guiding B Machines with CSP
To use this feature of ProB: first open a B Machine, then select "Use
CSP File to Guide B..." or "Use Default CSP File" in the "Open
@@ -116,4 +114,4 @@ guide the B machine with
(This feature is included since version 1.3.5-beta7.)
-==== References
+== References
diff --git a/src/docs/chapter/user/30_OtherLanguages/CSP/02_CSP-M_Syntax.adoc b/src/docs/chapter/user/30_OtherLanguages/CSP/02_CSP-M_Syntax.adoc
index 5046039..0e33a00 100644
--- a/src/docs/chapter/user/30_OtherLanguages/CSP/02_CSP-M_Syntax.adoc
+++ b/src/docs/chapter/user/30_OtherLanguages/CSP/02_CSP-M_Syntax.adoc
@@ -1,23 +1,23 @@
[[csp-m-syntax]]
-=== CSP-M Syntax
+= CSP-M Syntax
[[details-of-supported-csp-m-syntax]]
-==== Details of supported CSP-M syntax
+== Details of supported CSP-M syntax
Note: you can use the command "Summary of CSP syntax" in ProB's help
menu to get an up-to-date list of the supported syntax, along with
current limitations.
[[process-definitions]]
-==== PROCESS DEFINITIONS
+== PROCESS DEFINITIONS
* `Process = ProcessExpression`
[[process-expressions]]
-==== PROCESS EXPRESSIONS
+== PROCESS EXPRESSIONS
* `STOP` deadlocking process
* `SKIP` terminating process
@@ -54,7 +54,7 @@ empty)
* `let f1=E1 ... fk=Ek within P`
[[boolean-expressions]]
-==== BOOLEAN EXPRESSIONS
+== BOOLEAN EXPRESSIONS
* `true`
* `false`
@@ -73,7 +73,7 @@ empty)
* `elem(x,s)` sequence member check
[[value-expressions]]
-==== VALUE EXPRESSIONS
+== VALUE EXPRESSIONS
* `v+w`, `v-w` addition and subtraction
* `v*w` multiplication
@@ -106,13 +106,13 @@ explicit sequence for patterns)
* `set(s)` convert sequence into set
[[comments]]
-==== COMMENTS
+== COMMENTS
* `-- comment until end of line`
* `\{- arbitrary comment -}`
[[pragmas]]
-==== PRAGMAS
+== PRAGMAS
* `transparent f` where f is a unary function which will then on be
ignored by ProB
diff --git a/src/docs/chapter/user/30_OtherLanguages/CSP/03_Checking_CSP_Assertions.adoc b/src/docs/chapter/user/30_OtherLanguages/CSP/03_Checking_CSP_Assertions.adoc
index 09e4c3a..d4f3ccf 100644
--- a/src/docs/chapter/user/30_OtherLanguages/CSP/03_Checking_CSP_Assertions.adoc
+++ b/src/docs/chapter/user/30_OtherLanguages/CSP/03_Checking_CSP_Assertions.adoc
@@ -1,6 +1,6 @@
[[checking-csp-assertions]]
-=== Checking CSP Assertions
+= Checking CSP Assertions
As of version 1.3.4, ProB provides support for refinement checking and
various other assertions (deadlock, divergence, determinism, and LTL/CTL
@@ -11,7 +11,7 @@ assembled and checked in the _CSP Assertions Viewer_. A description of
the _CSP Assertions Viewer_ is also given.
[[supported-csp-assertions-in-prob]]
-==== Supported CSP Assertions in ProB
+== Supported CSP Assertions in ProB
ProB provides support for checking almost all types of CSP-M assertions
that can be checked within FDR2. Besides the assertion types that can be
@@ -144,7 +144,7 @@ syntax error. Bear in mind to remove or comment out such LTL/CTL
assertions in the CSP-M file before loading it in FDR2.
[[csp-assertions-viewer]]
-==== CSP Assertions Viewer
+== CSP Assertions Viewer
When a CSP-M specification is loaded one can open the _CSP Assertion
Viewer_ either from the menu bar of the main window by selecting the
@@ -392,7 +392,7 @@ button command “Cancel” is replaced by another button command
check when the button is clicked on.
[[debugging-non-satisfied-assertions]]
-==== Debugging Non-satisfied Assertions
+== Debugging Non-satisfied Assertions
In case an assertion check has failed the user can explore the reason
for the assertion violation. If the corresponding assertion is not
@@ -489,7 +489,7 @@ In the figure above, the nodes and the transitions of the respective
counterexample "a -> (b -> a)+" are colored in red.
[[checking-csp-assertions-with-probcli]]
-==== Checking CSP Assertions with `probcli`
+== Checking CSP Assertions with `probcli`
It is also possible to check CSP assertions with the command line
version of ProB. The command has the following syntax:
@@ -513,4 +513,4 @@ formula by means of a backslash \.
`probcli -csp_assertion "Q |= LTL: \"F [c]\"" example.csp`
-==== References and Notes
+== References and Notes
diff --git a/src/docs/chapter/user/30_OtherLanguages/CSP/ZZ_section_footer.adoc b/src/docs/chapter/user/30_OtherLanguages/CSP/ZZ_section_footer.adoc
new file mode 100644
index 0000000..909c09e
--- /dev/null
+++ b/src/docs/chapter/user/30_OtherLanguages/CSP/ZZ_section_footer.adoc
@@ -0,0 +1,2 @@
+
+:leveloffset: -1
diff --git a/src/docs/chapter/user/30_OtherLanguages/EventB/00_section_header.adoc b/src/docs/chapter/user/30_OtherLanguages/EventB/00_section_header.adoc
new file mode 100644
index 0000000..65bf970
--- /dev/null
+++ b/src/docs/chapter/user/30_OtherLanguages/EventB/00_section_header.adoc
@@ -0,0 +1,4 @@
+
+[[eventb-and-rodin]]
+= Event B and Rodin
+:leveloffset: +1
diff --git a/src/docs/chapter/user/30_OtherLanguages/EventB/01_Event-B.adoc b/src/docs/chapter/user/30_OtherLanguages/EventB/01_Event-B.adoc
index 61f7b22..68d8e04 100644
--- a/src/docs/chapter/user/30_OtherLanguages/EventB/01_Event-B.adoc
+++ b/src/docs/chapter/user/30_OtherLanguages/EventB/01_Event-B.adoc
@@ -1,12 +1,13 @@
+
[[event-b]]
-== Event-B
+= Event-B
-=== Installation and General Information
+== Installation and General Information
ProB supports animation and model-checking for Event-B specifications.
[[installation-event-b]]
-==== Installation
+=== Installation
To install the ProB plugin for http://www.event-b.org[Rodin], open the
_Help_ menu in Rodin and click "Install new software".
@@ -20,7 +21,7 @@ Alternativaly, one can use the Tcl/Tk version of ProB but Event-B models
must be exported to an .eventb file first (see below).
[[animation-and-modelchecking]]
-==== Animation and Modelchecking
+=== Animation and Modelchecking
You can start animation of a model (machine or context) by
right-clicking on the model in the Event-B explorer. Choose "Start
@@ -29,7 +30,7 @@ Animation / Model Checking".
//*TODO:* Here we should add more details about the ProB perspective and views.
[[export-for-use-with-the-tcltk-version-of-prob]]
-==== Export for use with the Tcl/Tk version of ProB
+=== Export for use with the Tcl/Tk version of ProB
You can export a model (machine or context) to an .eventb - file by
right-clicking on the model in the Event-B explorer. You can find the
@@ -39,7 +40,7 @@ Such a .eventb file can be opened by the command line and Tcl/Tk version
of ProB.
[[theories]]
-==== Theories
+=== Theories
ProB has (limited) support for theories.
@@ -54,7 +55,7 @@ Axiomatically defined operators are not supported without additional
annotations.
[[tagging-operators-event-b]]
-===== Tagging operators
+==== Tagging operators
ProB has some extra support for certain operators. ProB expects an
annotation to an operator that provides the information that it should
diff --git a/src/docs/chapter/user/30_OtherLanguages/EventB/02_Event-B_Theories.adoc b/src/docs/chapter/user/30_OtherLanguages/EventB/02_Event-B_Theories.adoc
index bbab389..588fcd1 100644
--- a/src/docs/chapter/user/30_OtherLanguages/EventB/02_Event-B_Theories.adoc
+++ b/src/docs/chapter/user/30_OtherLanguages/EventB/02_Event-B_Theories.adoc
@@ -1,5 +1,6 @@
+
[[event-b-theories]]
-=== Event-B Theories
+= Event-B Theories
ProB has (limited) support for theories.
@@ -14,7 +15,7 @@ Axiomatically defined operators are not supported without additional
annotations.
[[download-theories]]
-==== Download Theories
+== Download Theories
//An example project with theories: theories2.zip[] TODO: Downloadlink
@@ -57,7 +58,7 @@ BinaryTree::
Binary Trees are supported by ProB.
[[tagging-operators-event-b-theories]]
-==== Tagging operators
+== Tagging operators
[IMPORTANT]
*Please note:*
@@ -102,7 +103,7 @@ Nat
|=======================================================================
[[error-messages]]
-===== Error Messages
+=== Error Messages
In case the .ptm file is missing, you will get an error message such as
the following one:
diff --git a/src/docs/chapter/user/30_OtherLanguages/EventB/ProB_for_Event-B.adoc b/src/docs/chapter/user/30_OtherLanguages/EventB/ProB_for_Event-B.adoc
index d70712c..9f0ea98 100644
--- a/src/docs/chapter/user/30_OtherLanguages/EventB/ProB_for_Event-B.adoc
+++ b/src/docs/chapter/user/30_OtherLanguages/EventB/ProB_for_Event-B.adoc
@@ -1,5 +1,6 @@
+
[[prob-for-event-b]]
-=== ProB for Event-B
+= ProB for Event-B
In addition to classical B (aka B for software development), ProB also
supports Event-B and the Rodin platform. ProB can be installed as a
diff --git a/src/docs/chapter/user/30_OtherLanguages/EventB/ProB_for_Rodin.adoc b/src/docs/chapter/user/30_OtherLanguages/EventB/ProB_for_Rodin.adoc
index ffecd32..b38052e 100644
--- a/src/docs/chapter/user/30_OtherLanguages/EventB/ProB_for_Rodin.adoc
+++ b/src/docs/chapter/user/30_OtherLanguages/EventB/ProB_for_Rodin.adoc
@@ -1,10 +1,11 @@
+
[[prob-for-rodin]]
-=== ProB for Rodin
+= ProB for Rodin
Currently there are two versions of ProB available for Rodin.
[[prob-1-for-rodin]]
-==== ProB (1) for Rodin
+== ProB (1) for Rodin
The first one is based on the old Java API and supports
http://wiki.event-b.org/index.php/Rodin_Platform_2.8_Release_Notes[Rodin
@@ -16,7 +17,7 @@ Rodin>>. Nightly releases of this versions are also available on the
<<download,Download>> page.
[[prob-2.0-for-rodin]]
-==== ProB 2.0 for Rodin
+== ProB 2.0 for Rodin
The second, still experimental, one is based on the new
<<prob-java-api,ProB Java API>> (aka ProB 2.0). Because the UI
@@ -30,7 +31,7 @@ releases of this versions is also available on the
<<download,Download>> page.
[[multi-simulation-for-rodin-based-on-prob]]
-==== Multi-Simulation for Rodin based on ProB
+== Multi-Simulation for Rodin based on ProB
There is now also a
http://users.ecs.soton.ac.uk/vs2/ac.soton.multisim.updatesite/[Multi-Simulation
@@ -38,10 +39,10 @@ Plug-in] available for Rodin. It enables discrete/continuous
co-simulation.
[[other-plug-ins-for-rodin]]
-==== Other Plug-Ins for Rodin
+== Other Plug-Ins for Rodin
[[prover-evaluation]]
-===== Prover Evaluation
+=== Prover Evaluation
This Plug-in is available at the update site
http://nightly.cobra.cs.uni-duesseldorf.de/rodin_provereval/[http://nightly.cobra.cs.uni-duesseldorf.de/rodin_provereval/]
@@ -49,7 +50,7 @@ and is capable to evaluate a variety of provers or tactics on a
selection of proof obligations.
[[camille]]
-===== Camille
+=== Camille
We also develop the Camille text-editor for Rodin. A preliminary version
of Camille for Rodin 3.3 is available at the nightly update site:
diff --git a/src/docs/chapter/user/30_OtherLanguages/EventB/ZZ_section_footer.adoc b/src/docs/chapter/user/30_OtherLanguages/EventB/ZZ_section_footer.adoc
new file mode 100644
index 0000000..909c09e
--- /dev/null
+++ b/src/docs/chapter/user/30_OtherLanguages/EventB/ZZ_section_footer.adoc
@@ -0,0 +1,2 @@
+
+:leveloffset: -1
diff --git a/src/docs/chapter/user/30_OtherLanguages/ProZ.adoc b/src/docs/chapter/user/30_OtherLanguages/ProZ.adoc
index 6583324..9bd9df6 100644
--- a/src/docs/chapter/user/30_OtherLanguages/ProZ.adoc
+++ b/src/docs/chapter/user/30_OtherLanguages/ProZ.adoc
@@ -1,5 +1,6 @@
+
[[proz]]
-== ProZ
+= ProZ
ProZ is a extension
of the ProB animator and model checker to support Z specifications. It
@@ -11,7 +12,7 @@ https://www3.hhu.de/stups/downloads/pdf/proz07.pdf[iFM'07
article on ProZ] contains more details about the implementation.
[[preferences-for-proz]]
-=== Preferences
+== Preferences
A Z specification frequently makes use of comprehension sets, which are
often introduced by the underlying translation process from Z to B.
@@ -25,10 +26,10 @@ Animation Preferences ->
....
[[structure-of-the-z-specification]]
-=== Structure of the Z Specification
+== Structure of the Z Specification
[[state-and-initialization]]
-==== State and Initialization
+=== State and Initialization
To identify the components (like state, initialization, operations) of a
Z specification, ProZ expects a certain structure of the specification:
@@ -53,7 +54,7 @@ in the initialization, you can do that by including those schemas in the
predicate part.
[[operations]]
-===== Operations
+==== Operations
ProZ identifies schemas as operations if they satisfy the following
properties:
@@ -79,7 +80,7 @@ Then the schemas A,B and E describe all the same operation. F is also
identified as an operation that leaves the state unchanged.
[[axiomatic-definitions]]
-===== Axiomatic definitions
+==== Axiomatic definitions
If axiomatic definitions are present, the declared variables are treated
like constants. In the first step of the animation, ProB searches for
@@ -112,7 +113,7 @@ ProB will try to find a explicit set that will satisfy the given
property.
[[invariant]]
-===== Invariant
+==== Invariant
You can add a B-style invariant to the specification by defining a
schema "Invariant" that declares a subset of the state variables. In
@@ -120,7 +121,7 @@ each explored state the invariant will be checked. The model checking
feature of ProB will try to find states that violate the invariant.
[[scope-proz]]
-===== Scope
+==== Scope
It is possible to limit the search space of the model checker by adding
a schema "Scope" that declares a subset of the state variables. If
@@ -128,7 +129,7 @@ such a schema is present, each explored state is checked, if it
satisfies the predicate. If not, the state is not further explored.
[[abbreviation-definitions]]
-===== Abbreviation Definitions
+==== Abbreviation Definitions
Abbreviation definitions (e.g. Abbr == {1,2,3}) are used like macros by
ProZ. A reference to an abbreviation is replaced by its definition in a
@@ -139,7 +140,7 @@ definitions (\defs instead of ==) when defining state, initialization,
operations, etc.
[[graphical-animation-proz]]
-==== Graphical animation
+=== Graphical animation
(*Please note that this functionality is part of the next version. If
you want to use graphical animation, please download a version from the
@@ -191,10 +192,10 @@ Here is how the animation of the specification should look like:
image::ProZ_jars.png[]
[[special-constructs]]
-==== Special constructs
+=== Special constructs
[[prozignore]]
-===== prozignore
+==== prozignore
Sometimes it is not desired to check properties of some variables. E.g.
ProZ checks if the square function in 2.3.a is a total function by
@@ -236,7 +237,7 @@ It is also possible to append these lines to the "fuzzlib" in the fuzz
distribution.
[[translation-to-b]]
-===== Translation to B
+==== Translation to B
You can inspect the result of the translation process with "Show
internal representation" in the _Debug_ menu. Please note that the
@@ -248,7 +249,7 @@ shown B machine is normally not syntactically correct because of
* lack of support from the pretty printer for every construct
[[known-limitations]]
-==== Known Limitations
+=== Known Limitations
* Generic definitions are not supported yet.
* Miscellaneous unsupported constructs
@@ -257,22 +258,22 @@ shown B machine is normally not syntactically correct because of
* The error messages are not very helpful yet.
[[summary-of-supported-operators]]
-==== Summary of Supported Operators
+=== Summary of Supported Operators
....
-=== Logical predicates:
+== Logical predicates:
P \land Q conjunction
P \lor Q disjunction
P \implies Q implication
P \iff Q equivalence
\lnot P negation
-=== Quantifiers:
+== Quantifiers:
\forall x:T | P @ Q universal quantification (P => Q)
\exists x:T | P @ Q existential quantification (P & Q)
\exists_1 x:T | P @ Q exactly one existential quantification
-=== Sets:
+== Sets:
\emptyset empty set
\{E,F\} set extension
\{~x:S | P~\} set comprehension
@@ -288,13 +289,13 @@ shown B machine is normally not syntactically correct because of
\bigcup A generalized union of sets of sets
\bigcap A generalized intersection of sets of sets
-=== Pairs:
+== Pairs:
E \mapsto F pair
S \cross T Cartesian product
first E first part of pair
second E second part of pair
-=== Numbers:
+== Numbers:
\nat Natural numbers
\num Integers
\nat_1 Positive natural numbers
@@ -314,7 +315,7 @@ shown B machine is normally not syntactically correct because of
**: modulo of negative numbers not supported
-=== Functions:
+== Functions:
S \rel T relations
S \pfun T partial functions from S to T
S \fun T total functions from S to T
@@ -331,7 +332,7 @@ shown B machine is normally not syntactically correct because of
R \oplus Q overriding
R \plus transitive closure
-=== Sequences:
+== Sequences:
\langle E,... \rangle explicit sequence
\seq S sequences over S
\seq_1 S non-empty sequences
diff --git a/src/docs/chapter/user/30_OtherLanguages/TLA.adoc b/src/docs/chapter/user/30_OtherLanguages/TLA.adoc
index f43ed2c..2fb5a30 100644
--- a/src/docs/chapter/user/30_OtherLanguages/TLA.adoc
+++ b/src/docs/chapter/user/30_OtherLanguages/TLA.adoc
@@ -1,11 +1,12 @@
+
[[tla]]
-== TLA
+= TLA
As of version 1.3.5, ProB supports
http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html[TLA+].
[[using-prob-for-animation-and-model-checking-of-tla-specifications]]
-=== Using ProB for Animation and Model Checking of TLA+ specifications
+== Using ProB for Animation and Model Checking of TLA+ specifications
The http://nightly.cobra.cs.uni-duesseldorf.de/tcl/[latest version of
ProB] uses the translator TLA2B, which translates the non temporal part
@@ -32,7 +33,7 @@ also supports TLA syntax and you can experiment with its predicate and
expression evaluation capabilities.
[[tla2b]]
-=== TLA2B
+== TLA2B
The parser and semantic analyzer
http://research.microsoft.com/en-us/um/people/lamport/tla/sany.html[SANY]
@@ -63,7 +64,7 @@ under the ASSUME clause. TLA2B supports furthermore overriding of a
constant or definition by another definition in the configuration file.
[[supported-tla-syntax]]
-=== Supported TLA+ syntax
+== Supported TLA+ syntax
....
Logic
@@ -183,14 +184,14 @@ foo == ...
Init == ...
Next == ...
Spec == ...
-=====================
+====================
....
Temporal formulas and unused definitions are ignored by TLA2B (they are
also ignored by the type inference algorithm).
[[limitations-of-the-translation]]
-=== Limitations of the translation
+== Limitations of the translation
* due to the strict type system of the B method there are several
restrictions to TLA+ modules.
@@ -202,7 +203,7 @@ the tuple must have the same type
operator with arguments as argument (e.g.: `foo(bar(_),p)`)
[[tla-actions]]
-=== TLA+ Actions
+== TLA+ Actions
'''''
@@ -216,7 +217,7 @@ by ProB are not necessarily identical with the actions determined by
TLC.
[[understanding-the-type-checker]]
-=== Understanding the type checker
+== Understanding the type checker
Corresponding B types to TLA+ data values (let type(e) be the type of
the expression e):
diff --git a/src/docs/chapter/user/30_OtherLanguages/ZZ_section_footer.adoc b/src/docs/chapter/user/30_OtherLanguages/ZZ_section_footer.adoc
new file mode 100644
index 0000000..909c09e
--- /dev/null
+++ b/src/docs/chapter/user/30_OtherLanguages/ZZ_section_footer.adoc
@@ -0,0 +1,2 @@
+
+:leveloffset: -1
diff --git a/src/docs/chapter/user/40_AdvancedFeatures/00_Advanced_Features.adoc b/src/docs/chapter/user/40_AdvancedFeatures/00_section_header.adoc
similarity index 92%
rename from src/docs/chapter/user/40_AdvancedFeatures/00_Advanced_Features.adoc
rename to src/docs/chapter/user/40_AdvancedFeatures/00_section_header.adoc
index 9871f04..682deae 100644
--- a/src/docs/chapter/user/40_AdvancedFeatures/00_Advanced_Features.adoc
+++ b/src/docs/chapter/user/40_AdvancedFeatures/00_section_header.adoc
@@ -1,5 +1,7 @@
+
[[advanced-features]]
= Advanced Features
+:leveloffset: +1
Over the years, the ProB Team developed a few features for advanced users.
You can find further descriptions and tutorials on how to use them in the following sections.
diff --git a/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/00_section_header.adoc b/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/00_section_header.adoc
new file mode 100644
index 0000000..df0714c
--- /dev/null
+++ b/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/00_section_header.adoc
@@ -0,0 +1,4 @@
+
+[[feature-description]]
+= Feature Description
+:leveloffset: +1
diff --git a/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/01_Bash_Completion.adoc b/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/01_Bash_Completion.adoc
index 3bf1685..94353ac 100644
--- a/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/01_Bash_Completion.adoc
+++ b/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/01_Bash_Completion.adoc
@@ -1,5 +1,6 @@
+
[[bash-completion]]
-== Bash Completion
+= Bash Completion
For the http://en.wikipedia.org/wiki/Bash_(Unix_shell)[Bash] Unix Shell
we provide command completion support.
@@ -12,7 +13,7 @@ $ probcli -re
....
[[installation-bash-completion]]
-=== Installation
+== Installation
A generated version of the command completion for Bash is available
http://nightly.cobra.cs.uni-duesseldorf.de/bash/prob_completion.sh[here].
@@ -28,7 +29,7 @@ settings, e.g. in the *.bashrc* or *.profile* files in your home
directory.
[[contributing]]
-=== Contributing
+== Contributing
Bugs and improvements can be submitted on the project's
https://github.com/bivab/prob_bash_completion[GitHub Page]
diff --git a/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/02_Common_Subexpression_Elimination.adoc b/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/02_Common_Subexpression_Elimination.adoc
index c969797..269c272 100644
--- a/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/02_Common_Subexpression_Elimination.adoc
+++ b/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/02_Common_Subexpression_Elimination.adoc
@@ -1,12 +1,13 @@
+
[[common-subexpression-elimination]]
-== Common Subexpression Elimination
+= Common Subexpression Elimination
As of version 1.5.1 ProB supports
https://en.wikipedia.org/wiki/Common_subexpression_elimination[common
subexpression elimination (CSE)].
[[basics-of-cse]]
-=== Basics of CSE
+== Basics of CSE
To enable CSE you need to set the advanced preference `CSE` to true
(this can be done using the switch `-p CSE TRUE` when using the
@@ -50,7 +51,7 @@ well-definedness (e.g., suppose a is not in the domain of f) and for
performance.
[[substitutions]]
-=== Substitutions
+== Substitutions
To enable CSE also inside substitutions (aka B statements) you need to
set the preference `CSE_SUBST` to true. By default, the CSE will only be
@@ -59,7 +60,7 @@ the properties or individual predicates inside operations (but not the
operation as a whole).
[[sharing-predicates]]
-=== Sharing Predicates
+== Sharing Predicates
By default ProB's CSE will also share predicates. You can turn off CSE
for predicates, i.e., only expressions get shared, by setting the
@@ -77,7 +78,7 @@ After setting `CSE_PRED` to `FALSE`, this will be translated into:
`LET @0==(x + 1) IN @0 > 10 & (@0 > 10 => y = 22)`
[[other-preferences]]
-=== Other Preferences
+== Other Preferences
ProB will also share expressions which are potentially not well-defined,
and takes extra care with those expressions (in particular in the
@@ -96,7 +97,7 @@ and ProB will find the solution `x=4`. With `CSE_WD_ONLY` to `TRUE`, the
predicate will be left unchanged (and ProB will find the same solution).
[[tips]]
-=== Tips
+== Tips
To inspect the effect of CSE, you do one of the following:
diff --git a/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/03_PROBPATH.adoc b/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/03_PROBPATH.adoc
index 6c9e950..8a4bbc7 100644
--- a/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/03_PROBPATH.adoc
+++ b/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/03_PROBPATH.adoc
@@ -1,5 +1,6 @@
+
[[probpath]]
-== PROBPATH
+= PROBPATH
Starting with version 1.5 of ProB, it is possible to customize where the
parser will ProB will search for referenced files.
diff --git a/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/04_TLC.adoc b/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/04_TLC.adoc
index 18a2b52..d5214c4 100644
--- a/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/04_TLC.adoc
+++ b/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/04_TLC.adoc
@@ -1,5 +1,6 @@
+
[[tlc]]
-== TLC
+= TLC
As of version 1.4.0, ProB can make use of
http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html[TLC]
@@ -13,10 +14,10 @@ http://research.microsoft.com/en-us/um/people/lamport/tla/license.html[MIT
License].
[[how-to-use-tlc]]
-=== How to use TLC
+== How to use TLC
[[using-tlc-in-prob-tcltk]]
-==== Using TLC in ProB Tcl/Tk
+=== Using TLC in ProB Tcl/Tk
First you have to open a B specification in the ProB GUI. Then you can
select the menu command "Model Check with TLC" in the
@@ -43,7 +44,7 @@ pane) to give an optimal feedback.
image::Model_Checking_With_TLC_Trace.png[]
[[requirements]]
-===== Requirements
+==== Requirements
On Linux the tlc-thread package is required to run TLC from the tcl/tk
ui:
@@ -51,7 +52,7 @@ ui:
`sudo apt-get install tcl-thread`
[[using-tlc-in-probcli]]
-==== Using TLC in probcli
+=== Using TLC in probcli
You can use the following switch to use TLC rather than ProB's model
checker:
@@ -75,7 +76,7 @@ be used by TLC. So, a call might look like this:
`probcli FILE.mch -mc_with_tlc -p TLC_WORKERS 2 -noltl`
[[when-to-use-tlc]]
-=== When to use TLC
+== When to use TLC
TLC is extremely valuable when it comes to explicit state model checking
for large state spaces. Otherwise, TLC has no constraint solving
@@ -100,7 +101,7 @@ http://stups.hhu.de/w/Special:Publication/HansenLeuschel_TLC4B_techreport[techni
report] that describes our translation from B to TLA+.
[[limitations-tlc]]
-=== Limitations
+== Limitations
The following constructs are currently not supported by the TLC4B
translator:
@@ -110,7 +111,7 @@ translator:
* Sequential composition statement (G;H)
[[visited-states]]
-=== Visited States
+== Visited States
Sometimes TLC will show a different number of visited states compared to
the ProB model checker. The following example should illustrate this
@@ -136,7 +137,7 @@ image::NumberOfStates.jpeg[]
TLC will only report 10 distinct states (10 initialization states).
[[more-information]]
-=== More Information
+== More Information
More information can be found in our
https://www3.hhu.de/stups/downloads/pdf/HansenLeuschel_ABZ14.pdf[ABZ'14
diff --git a/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/ZZ_section_footer.adoc b/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/ZZ_section_footer.adoc
new file mode 100644
index 0000000..909c09e
--- /dev/null
+++ b/src/docs/chapter/user/40_AdvancedFeatures/01_Feature_Description/ZZ_section_footer.adoc
@@ -0,0 +1,2 @@
+
+:leveloffset: -1
diff --git a/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/00_section_header.adoc b/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/00_section_header.adoc
new file mode 100644
index 0000000..de7acf4
--- /dev/null
+++ b/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/00_section_header.adoc
@@ -0,0 +1,4 @@
+
+[[using-prob]]
+= Using ProB
+:leveloffset: +1
diff --git a/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Generating_Documents_with_ProB_and_Latex.adoc b/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Generating_Documents_with_ProB_and_Latex.adoc
index 43868c2..5e70f08 100644
--- a/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Generating_Documents_with_ProB_and_Latex.adoc
+++ b/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Generating_Documents_with_ProB_and_Latex.adoc
@@ -1,12 +1,13 @@
+
[[generating-documents-with-prob-and-latex]]
-== Generating Documents with ProB and Latex
+= Generating Documents with ProB and Latex
ProB can (as of version 1.6.1) be used to process Latex files, i.e., the
command-line tool probcli scans a given Latex file and replaces certain
commands by processed results.
[[usage-generating-documents]]
-=== Usage
+== Usage
A typical usage would be as follows:
@@ -33,7 +34,7 @@ features:
https://www3.hhu.de/stups/prob/images/7/7f/Prob_latex_doc.pdf[ProB Latex Documentation]
[[commands]]
-=== Commands
+== Commands
The commands are described in the PDF document above. Here is a short
summary of some of the commands:
@@ -94,7 +95,7 @@ for every element of the set expression, setting the identifier to a
value of the set.
[[some-examples]]
-=== Some Examples
+== Some Examples
* Presentation held in Grenoble in September 2016 about "Constraint
Programming Puzzles in B"
diff --git a/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_Atelier_B.adoc b/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_Atelier_B.adoc
index 6fd21b0..0fdd957 100644
--- a/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_Atelier_B.adoc
+++ b/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_Atelier_B.adoc
@@ -1,12 +1,13 @@
+
[[using-prob-with-atelier-b]]
-== Using ProB with Atelier B
+= Using ProB with Atelier B
As of version 1.3,
ProB contains a much improved parser which tries be compliant with
Atelier B as much as possible.
[[atelier-b-plugin]]
-=== Atelier B Plugin
+== Atelier B Plugin
There is also a
http://tools.clearsy.com/tools/atelier-b-4-0-gui/external-tools-integration/prob-etool-generation/[plugin
@@ -14,10 +15,10 @@ for Atelier B] for use withthe standalone Tcl/Tk Version on
http://www.atelierb.eu/[Atelier B] projects.
[[differences-with-atelier-b]]
-=== Differences with Atelier B
+== Differences with Atelier B
[[extra-features-of-prob]]
-==== Extra Features of ProB
+=== Extra Features of ProB
* Identifiers: ProB also allows identifiers consisting of a single
letter. ProB also accepts enumerated set elements to be used as
@@ -59,7 +60,7 @@ machines
around it: `(IF x<0 THEN -x ELSE x END)`
[[limitations-with-atelierb]]
-==== Limitations
+=== Limitations
* Parsing: ProB will require parentheses around the comma, the
relational composition, and parallel product operators. For example, you
diff --git a/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_KODKOD.adoc b/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_KODKOD.adoc
index bcca0e0..bfea468 100644
--- a/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_KODKOD.adoc
+++ b/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_KODKOD.adoc
@@ -1,5 +1,6 @@
+
[[using-prob-with-kodkod]]
-== Using ProB with KODKOD
+= Using ProB with KODKOD
As of version 1.3.5 ProB can make use of
http://alloy.mit.edu/kodkod/[Kodkod] as an alternate way of solving
@@ -7,7 +8,7 @@ constraints. Kodkod provides a relational interface to SAT solvers and
is the heart of the http://alloy.mit.edu/alloy/[Alloy] tool.
[[how-to-enable-kodkod]]
-=== How to enable Kodkod
+== How to enable Kodkod
For the command-line version you need to call prob as follows:
@@ -27,7 +28,7 @@ For the ProB Tcl/Tk Version you should select the menu command "Enable
Kodkod for Properties" in the _Preferences_ menu.
[[what-can-be-translated-kodkod]]
-=== What can be translated
+== What can be translated
* Types:
** Basic Types: Deferred Sets, enumerated sets, integers, booleans
@@ -53,7 +54,7 @@ analysis can estimate the interval of its possible values.
unless you set the `KODKOD_ONLY_FULL` preference to FALSE.
[[when-is-the-kokod-translation-used]]
-=== When is the Kokod translation used
+== When is the Kokod translation used
Once enabled, the Kodkod translation will be used in the following
circumstances:
@@ -67,7 +68,7 @@ _Verify_ -> Constraint-Based Checking)
* for the REPL in probcli (`probcli -p KODKOD TRUE -repl`)
[[sat-solver]]
-=== SAT solver
+== SAT solver
By default Kodkod in ProB uses the bundled SAT4J solver. You can switch
to using minisat by putting a current version of `libminisat.jnilib`
@@ -85,7 +86,7 @@ These files can be downloaded from the
http://alloy.mit.edu/kodkod/download.html[Kodkod download site].
[[more-preferences]]
-=== More Preferences
+== More Preferences
If you set `KODKOD_ONLY_FULL` to `FALSE`, then the Kodkod translation
can be applied to part of a predicate. In other words, the predicate
@@ -107,7 +108,7 @@ interested in only one solution and `KODKOD_ONLY_FULL` is `TRUE`, then
you should set this value to 1.
[[more-details-on-kodkod]]
-=== More details
+== More details
* https://www3.hhu.de/stups/downloads/pdf/PlaggeLeuschel_Kodkod2012.pdf[Plagge,
Leuschel. Validating B, Z and TLA+ using ProB and Kodkod. In Proceedings
diff --git a/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_Z3.adoc b/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_Z3.adoc
index c40f980..4c66329 100644
--- a/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_Z3.adoc
+++ b/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/Using_ProB_with_Z3.adoc
@@ -1,12 +1,13 @@
+
[[using-prob-with-z3]]
-== Using ProB with Z3
+= Using ProB with Z3
The current nightly versions of ProB can make use of
https://github.com/Z3Prover/z3[Z3] as an alternate way of solving
constraints.
[[how-to-use-z3-within-prob]]
-=== How to use Z3 within ProB
+== How to use Z3 within ProB
One can start a REPL (Read-Eval-Print-Loop) by starting probcli with the
`-repl` command line option. Any predicate preceded with `:z3` will be
@@ -18,7 +19,7 @@ enabled by setting the corresponding preference by passing
on the command line.
[[how-to-install-z3-for-prob]]
-=== How to install Z3 for ProB
+== How to install Z3 for ProB
First of all, download a nightly build of ProB from the
<<download,Downloads>> page. To connect Z3 to ProB you also need the
@@ -47,7 +48,7 @@ can not be loaded, ProB will answer with "solver_not_available" when
Z3 is queried.
[[what-can-be-translated-z3]]
-=== What can be translated
+== What can be translated
Currently, the Z3 translation is unable to cope with the following
constructs:
@@ -67,7 +68,7 @@ When used together with ProB, everything Z3 can not be coped with will
be handled by ProB alone automatically.
[[examples-z3]]
-=== Examples
+== Examples
Using the repl, one can try out different examples.
diff --git a/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/ZZ_section_footer.adoc b/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/ZZ_section_footer.adoc
new file mode 100644
index 0000000..909c09e
--- /dev/null
+++ b/src/docs/chapter/user/40_AdvancedFeatures/02_Using_ProB/ZZ_section_footer.adoc
@@ -0,0 +1,2 @@
+
+:leveloffset: -1
diff --git a/src/docs/chapter/user/40_AdvancedFeatures/ZZ_section_footer.adoc b/src/docs/chapter/user/40_AdvancedFeatures/ZZ_section_footer.adoc
new file mode 100644
index 0000000..909c09e
--- /dev/null
+++ b/src/docs/chapter/user/40_AdvancedFeatures/ZZ_section_footer.adoc
@@ -0,0 +1,2 @@
+
+:leveloffset: -1
diff --git a/src/docs/chapter/user/50_ProB2/00_ProB2.adoc b/src/docs/chapter/user/50_ProB2/00_section_header.adoc
similarity index 56%
rename from src/docs/chapter/user/50_ProB2/00_ProB2.adoc
rename to src/docs/chapter/user/50_ProB2/00_section_header.adoc
index 349d5b3..a26ea87 100644
--- a/src/docs/chapter/user/50_ProB2/00_ProB2.adoc
+++ b/src/docs/chapter/user/50_ProB2/00_section_header.adoc
@@ -1,2 +1,4 @@
+
[[prob2.0]]
= ProB 2.0
+:leveloffset: +1
diff --git a/src/docs/chapter/user/50_ProB2/01_ProB_2.0_Development.adoc b/src/docs/chapter/user/50_ProB2/01_ProB_2.0_Development.adoc
index a6e47a2..20943a1 100644
--- a/src/docs/chapter/user/50_ProB2/01_ProB_2.0_Development.adoc
+++ b/src/docs/chapter/user/50_ProB2/01_ProB_2.0_Development.adoc
@@ -1,11 +1,12 @@
+
[[prob2.0_general]]
-== General
+= General
[[prob2.0-development]]
-== ProB 2.0 Development
+= ProB 2.0 Development
[[basic-design-principles]]
-=== Basic Design Principles
+== Basic Design Principles
One of our main design goals was that we wanted to build our UI on top
of a programmatic API. Our goal was to bring the ProB 2.0 API into a
@@ -29,7 +30,7 @@ spent quite a bit of energy developing a developer friendly console for
testing out features as they are being developed.
[[why-groovy]]
-=== Why Groovy?
+== Why Groovy?
The scripting language that we chose is Groovy. It is a dynamically
typed JVM language. Because of the seamless integration between Java and
@@ -45,7 +46,7 @@ ProB 2.0, we redefined the java.lang.String class so that we can specify
the correct Parser with which a string should be parsed.
[[explanation-of-the-basic-programmatic-abstractions]]
-=== Explanation of the basic programmatic abstractions
+== Explanation of the basic programmatic abstractions
The basic programmatic abstractions that are available in the ProB 2.0
API are the Model, Trace, and StateSpace abstractions. The Model
@@ -57,7 +58,7 @@ different is available
<<programmatic-abstractions-in-the-prob-2.0-api,here>>.
[[tutorial-of-the-current-features-of-prob-2.0]]
-=== Tutorial of the Current Features of ProB 2.0
+== Tutorial of the Current Features of ProB 2.0
A tutorial for the current features of ProB 2.0 is available
<<prob2-tutorial,here>>.
diff --git a/src/docs/chapter/user/50_ProB2/02_ProB_2.0_within_Rodin_and_a_HTML_Visualization_Example.adoc b/src/docs/chapter/user/50_ProB2/02_ProB_2.0_within_Rodin_and_a_HTML_Visualization_Example.adoc
index c4d450d..f8e2ec4 100644
--- a/src/docs/chapter/user/50_ProB2/02_ProB_2.0_within_Rodin_and_a_HTML_Visualization_Example.adoc
+++ b/src/docs/chapter/user/50_ProB2/02_ProB_2.0_within_Rodin_and_a_HTML_Visualization_Example.adoc
@@ -1,8 +1,9 @@
+
[[prob2-within-rodin]]
-== ProB 2.0 within Rodin
+= ProB 2.0 within Rodin
[[installing-prob-2.0-from-rodin-2.7-or-later]]
-=== Installing ProB 2.0 from Rodin 2.7 or later
+== Installing ProB 2.0 from Rodin 2.7 or later
ProB 2.0 for Rodin 3.1 can be installed from the update site, which is located
http://nightly.cobra.cs.uni-duesseldorf.de/prob2/updates/releases/advance-final/[here].
@@ -19,7 +20,7 @@ image::Install_prob2.png[]
and install the ProB 2.0 plugin
[[obtaining-the-latest-prob-binary]]
-=== Obtaining the latest ProB binary
+== Obtaining the latest ProB binary
Open a Groovy Console and type `upgrade latest`.
@@ -31,14 +32,14 @@ binary and the lib directory into a `.prob` directory in your home
directory.
[[import-the-lift-project]]
-=== Import the Lift Project
+== Import the Lift Project
Select the Rodin `Import…` menu command and import the
#FIXME Lift.zip LINK.
[[start-animating-the-lift]]
-=== Start Animating the Lift
+== Start Animating the Lift
Right-click on the `MLift` model and select the `Start Animation`
command:
@@ -50,7 +51,7 @@ Click on setup_constants and initialise in the Events view:
image::MLiftEventsView.png[]
[[open-html-visualization]]
-=== Open HTML Visualization
+== Open HTML Visualization
Go into the BMotion Studio Menu at the top and select
`Open BMotion Studio Template`:
diff --git a/src/docs/chapter/user/50_ProB2/Prob2-advance-release.adoc b/src/docs/chapter/user/50_ProB2/Prob2-advance-release.adoc
index 078eaba..c91ac60 100644
--- a/src/docs/chapter/user/50_ProB2/Prob2-advance-release.adoc
+++ b/src/docs/chapter/user/50_ProB2/Prob2-advance-release.adoc
@@ -1,4 +1,6 @@
-== ProB 2.0 Advanced Release
+
+[[prob2.0_advanced_release]]
+= ProB 2.0 Advanced Release
ProB 2.0 for Rodin 3.1 can be installed from the update site located at:
http://nightly.cobra.cs.uni-duesseldorf.de/prob2/updates/releases/advance-final/
diff --git a/src/docs/chapter/user/50_ProB2/ZZ_section_footer.adoc b/src/docs/chapter/user/50_ProB2/ZZ_section_footer.adoc
new file mode 100644
index 0000000..909c09e
--- /dev/null
+++ b/src/docs/chapter/user/50_ProB2/ZZ_section_footer.adoc
@@ -0,0 +1,2 @@
+
+:leveloffset: -1
diff --git a/src/docs/chapter/user/51_JavaFX/00_section_header.adoc b/src/docs/chapter/user/51_JavaFX/00_section_header.adoc
new file mode 100644
index 0000000..ee6bdf7
--- /dev/null
+++ b/src/docs/chapter/user/51_JavaFX/00_section_header.adoc
@@ -0,0 +1,4 @@
+
+[[prob-2.0-javafx-ui]]
+= ProB 2.0 JavaFX UI
+:leveloffset: +1
diff --git a/src/docs/chapter/user/50_ProB2/JavaFX/01_ProB2_JavaFX_UI.adoc b/src/docs/chapter/user/51_JavaFX/01_ProB2_JavaFX_UI.adoc
similarity index 93%
rename from src/docs/chapter/user/50_ProB2/JavaFX/01_ProB2_JavaFX_UI.adoc
rename to src/docs/chapter/user/51_JavaFX/01_ProB2_JavaFX_UI.adoc
index 8c4eff8..90bc360 100644
--- a/src/docs/chapter/user/50_ProB2/JavaFX/01_ProB2_JavaFX_UI.adoc
+++ b/src/docs/chapter/user/51_JavaFX/01_ProB2_JavaFX_UI.adoc
@@ -1,11 +1,11 @@
-[[prob2-javafx-ui]]
-== ProB 2.0 JavaFX UI
+[[beta-version-download]]
+= Beta Version Download
* A beta version of this new UI is available at
https://www3.hhu.de/stups/downloads/prob2/[https://www3.hhu.de/stups/downloads/prob2/].
[[the-prob2-javafx-main-window]]
-=== The ProB2 JavaFX Main Window
+== The ProB2 JavaFX Main Window
By default the main window is split into three vertical panes (see
below).
@@ -25,12 +25,12 @@ activate:
image::ProB2JavaFX_UI_Overview.png[]
[[the-prob2-javafx-main-menu-bar]]
-=== The ProB2 JavaFX Main Menu Bar
+== The ProB2 JavaFX Main Menu Bar
The menu bar contains the various commands to access the features of
ProB. It includes the following menus:
-==== File
+=== File
image::File.png[]
@@ -39,7 +39,7 @@ Project, open an existing project or a machine, open recent projects
shown as list and/or clear the list of recent projects, close the ProB2
JavaFX UI, save your project or reload the currently running machine.
-==== Edit
+=== Edit
image::Edit.png[]
@@ -48,20 +48,20 @@ current machine (either in the editor provided by the ProB2 JavaFX UI or
in the your operating systems standard editor) and allows to edit your
general and global preferences by opening a seperate window.
-==== Formula
+=== Formula
image::Formula.png[]
Here you can add formulas for visualization and
open the history chart window.
-==== Consoles
+=== Consoles
image::Consoles.png[]
This submenu leads to two consoles, one Groovy, one B.
-==== Perspectives
+=== Perspectives
image::Perspectives.png[]
@@ -73,13 +73,13 @@ windows. _Load_ allows you to make your own perspective by providing an
FXML file containing the views but be aware that this might ruin the
ability to detach components.
-==== View
+=== View
image::View.png[]
This submenu allows you to adjust font and button size in the ProB2 JavaFX UI.
-==== Help
+=== Help
image::Help.png[]
diff --git a/src/docs/chapter/user/50_ProB2/JavaFX/11_History_View.adoc b/src/docs/chapter/user/51_JavaFX/11_History_View.adoc
similarity index 97%
rename from src/docs/chapter/user/50_ProB2/JavaFX/11_History_View.adoc
rename to src/docs/chapter/user/51_JavaFX/11_History_View.adoc
index 7eabba2..97f456c 100644
--- a/src/docs/chapter/user/50_ProB2/JavaFX/11_History_View.adoc
+++ b/src/docs/chapter/user/51_JavaFX/11_History_View.adoc
@@ -1,5 +1,6 @@
+
[[javafx-history-view]]
-== History View
+= History View
image::History.png[]
diff --git a/src/docs/chapter/user/50_ProB2/JavaFX/12_Project_View.adoc b/src/docs/chapter/user/51_JavaFX/12_Project_View.adoc
similarity index 95%
rename from src/docs/chapter/user/50_ProB2/JavaFX/12_Project_View.adoc
rename to src/docs/chapter/user/51_JavaFX/12_Project_View.adoc
index e946856..ac1820b 100644
--- a/src/docs/chapter/user/50_ProB2/JavaFX/12_Project_View.adoc
+++ b/src/docs/chapter/user/51_JavaFX/12_Project_View.adoc
@@ -1,5 +1,6 @@
+
[[javafx-project-view]]
-== Project View
+= Project View
If no machine or no project has been opened, the Project View will allow
you to create a project. If you choose to open a machine without having
@@ -15,7 +16,7 @@ The Project View contains several tabs:
(each pair has its own entry)
[[javafx-project-tab]]
-=== Project Tab
+== Project Tab
image::Project_Tab.png[]
@@ -25,7 +26,7 @@ opening a machine or chosen by the user who manually created the project
and can be changed by double clicking on each respectively.
[[javafx-machines-tab]]
-=== Machines Tab
+== Machines Tab
image::Machines_Tab.png[]
@@ -35,7 +36,7 @@ the project. By clicking right on a specific machine this machine can be
edited or removed from the project.
[[javafx-verifications-tab]]
-=== Verifications Tab
+== Verifications Tab
image::Verifications_Tab.png[] This tab shows the status of each type
of verification run on the machines contained by the project. If no test
@@ -45,7 +46,7 @@ green check will be displayed. If a test failed, a red x sign will be
shown.
[[javafx-preferences-tab]]
-=== Preferences Tab
+== Preferences Tab
image::Preferences_Tab.png[]
@@ -59,7 +60,7 @@ image::Add_Preference.png[]
The screenshot above shows the window for adding and editing preferences.
[[javafx-run-configurations-tab]]
-=== Run Configurations Tab
+== Run Configurations Tab
image::Runconfigurations_Tab.png[]
diff --git a/src/docs/chapter/user/50_ProB2/JavaFX/13_Verification_View.adoc b/src/docs/chapter/user/51_JavaFX/13_Verification_View.adoc
similarity index 92%
rename from src/docs/chapter/user/50_ProB2/JavaFX/13_Verification_View.adoc
rename to src/docs/chapter/user/51_JavaFX/13_Verification_View.adoc
index 6a557e4..6f88c4e 100644
--- a/src/docs/chapter/user/50_ProB2/JavaFX/13_Verification_View.adoc
+++ b/src/docs/chapter/user/51_JavaFX/13_Verification_View.adoc
@@ -1,5 +1,6 @@
+
[[javafx-verification-view]]
-== Verification View
+= Verification View
The Verification View provides 3 different methods to test a machine:
@@ -12,7 +13,7 @@ machine and interrupt the checking process by pressing the "Cancel"
button.
[[javafx-modelchecking]]
-=== Modelchecking
+== Modelchecking
image::Modelchecking.png[]
@@ -28,7 +29,7 @@ By pushing the `Model Check` button your selected variant will be
added to the list shown at the top of the Modelchecking Tab.
[[javafx-ltl-verifications]]
-=== LTL Verifications
+== LTL Verifications
image::LTL.png[]
@@ -37,7 +38,7 @@ Pattern` buttons an editor for each respectively will be opened and you
can add LTL formulas or patterns to the lists to be checked for.
[[javafx-constraint-based-checking]]
-=== Constraint Based Checking
+== Constraint Based Checking
image::CBC.png[]
diff --git a/src/docs/chapter/user/50_ProB2/JavaFX/14_Statistics_View.adoc b/src/docs/chapter/user/51_JavaFX/14_Statistics_View.adoc
similarity index 93%
rename from src/docs/chapter/user/50_ProB2/JavaFX/14_Statistics_View.adoc
rename to src/docs/chapter/user/51_JavaFX/14_Statistics_View.adoc
index 2f49b23..5525b4c 100644
--- a/src/docs/chapter/user/50_ProB2/JavaFX/14_Statistics_View.adoc
+++ b/src/docs/chapter/user/51_JavaFX/14_Statistics_View.adoc
@@ -1,5 +1,6 @@
+
[[javafx-statistics-view]]
-== Statistics View
+= Statistics View
The Statistics View provides some state and transition data: The main
view shows the quantity of processed states and total transitions, the
diff --git a/src/docs/chapter/user/51_JavaFX/ZZ_section_footer.adoc b/src/docs/chapter/user/51_JavaFX/ZZ_section_footer.adoc
new file mode 100644
index 0000000..909c09e
--- /dev/null
+++ b/src/docs/chapter/user/51_JavaFX/ZZ_section_footer.adoc
@@ -0,0 +1,2 @@
+
+:leveloffset: -1
diff --git a/src/docs/chapter/developer/20_prolog/00_section_header.adoc b/src/docs/chapter/user/52_Prolog/00_section_header.adoc
similarity index 61%
rename from src/docs/chapter/developer/20_prolog/00_section_header.adoc
rename to src/docs/chapter/user/52_Prolog/00_section_header.adoc
index a6ef146..c51697c 100644
--- a/src/docs/chapter/developer/20_prolog/00_section_header.adoc
+++ b/src/docs/chapter/user/52_Prolog/00_section_header.adoc
@@ -1,2 +1,4 @@
+
+[[prob-prolog-guide]]
= ProB Prolog Guide
:leveloffset: +1
diff --git a/src/docs/chapter/developer/20_prolog/Organization_of_ProB_Sources.adoc b/src/docs/chapter/user/52_Prolog/Organization_of_ProB_Sources.adoc
similarity index 98%
rename from src/docs/chapter/developer/20_prolog/Organization_of_ProB_Sources.adoc
rename to src/docs/chapter/user/52_Prolog/Organization_of_ProB_Sources.adoc
index 7ad6647..c38d374 100644
--- a/src/docs/chapter/developer/20_prolog/Organization_of_ProB_Sources.adoc
+++ b/src/docs/chapter/user/52_Prolog/Organization_of_ProB_Sources.adoc
@@ -1,3 +1,4 @@
+
[[organization-of-prob-sources]]
= Organization of ProB Sources
diff --git a/src/docs/chapter/developer/20_prolog/ProB's_Prolog_Datastructures.adoc b/src/docs/chapter/user/52_Prolog/ProB's_Prolog_Datastructures.adoc
similarity index 99%
rename from src/docs/chapter/developer/20_prolog/ProB's_Prolog_Datastructures.adoc
rename to src/docs/chapter/user/52_Prolog/ProB's_Prolog_Datastructures.adoc
index a396eee..db58607 100644
--- a/src/docs/chapter/developer/20_prolog/ProB's_Prolog_Datastructures.adoc
+++ b/src/docs/chapter/user/52_Prolog/ProB's_Prolog_Datastructures.adoc
@@ -1,3 +1,4 @@
+
[[probs-prolog-datastructures]]
= ProB's Prolog Datastructures
diff --git a/src/docs/chapter/developer/20_prolog/Prolog_Coding_Guidelines.adoc b/src/docs/chapter/user/52_Prolog/Prolog_Coding_Guidelines.adoc
similarity index 98%
rename from src/docs/chapter/developer/20_prolog/Prolog_Coding_Guidelines.adoc
rename to src/docs/chapter/user/52_Prolog/Prolog_Coding_Guidelines.adoc
index 818ae06..e88baad 100644
--- a/src/docs/chapter/developer/20_prolog/Prolog_Coding_Guidelines.adoc
+++ b/src/docs/chapter/user/52_Prolog/Prolog_Coding_Guidelines.adoc
@@ -1,3 +1,4 @@
+
[[prolog-coding-guidelines]]
= Prolog Coding Guidelines
@@ -97,7 +98,7 @@ especially when you only have one real commit.
* avoid merge bombs with many changed files: a Git merge can hide unintended changes,
e.g., accidentally reverting previous commits because of editor issues (editor out of sync with file system).
* provide good commit messages. If a commit is related to a JIRA ticket
-reference the identifier of the ticket in the commit message.
+reference the identifier of the ticket in the commit message.
https://chris.beams.io/posts/git-commit/[This web page] provides the following seven rules:
* Separate subject from body with a blank line
* Limit the subject line to 50 characters
@@ -106,7 +107,7 @@ https://chris.beams.io/posts/git-commit/[This web page] provides the following s
* Use the imperative mood in the subject line
* Wrap the body at 72 characters
* Use the body to explain what and why vs. how
-
+
[[useful-bash-aliases]]
Useful Bash Aliases
diff --git a/src/docs/chapter/developer/20_prolog/Running_ProB_from_source.adoc b/src/docs/chapter/user/52_Prolog/Running_ProB_from_source.adoc
similarity index 99%
rename from src/docs/chapter/developer/20_prolog/Running_ProB_from_source.adoc
rename to src/docs/chapter/user/52_Prolog/Running_ProB_from_source.adoc
index a5385d7..53a6c93 100644
--- a/src/docs/chapter/developer/20_prolog/Running_ProB_from_source.adoc
+++ b/src/docs/chapter/user/52_Prolog/Running_ProB_from_source.adoc
@@ -1,3 +1,4 @@
+
[[running-prob-from-source]]
= Running ProB from source
diff --git a/src/docs/chapter/developer/20_prolog/Why_Prolog.adoc b/src/docs/chapter/user/52_Prolog/Why_Prolog.adoc
similarity index 99%
rename from src/docs/chapter/developer/20_prolog/Why_Prolog.adoc
rename to src/docs/chapter/user/52_Prolog/Why_Prolog.adoc
index dacdfb8..bbde80b 100644
--- a/src/docs/chapter/developer/20_prolog/Why_Prolog.adoc
+++ b/src/docs/chapter/user/52_Prolog/Why_Prolog.adoc
@@ -1,5 +1,4 @@
-
[[why-prolog]]
= Why Prolog?
diff --git a/src/docs/chapter/user/52_Prolog/ZZ_section_footer.adoc b/src/docs/chapter/user/52_Prolog/ZZ_section_footer.adoc
new file mode 100644
index 0000000..909c09e
--- /dev/null
+++ b/src/docs/chapter/user/52_Prolog/ZZ_section_footer.adoc
@@ -0,0 +1,2 @@
+
+:leveloffset: -1
diff --git a/src/docs/chapter/user/55_JavaAPI/00_JavaAPI.adoc b/src/docs/chapter/user/55_JavaAPI/00_JavaAPI.adoc
deleted file mode 100644
index fef9815..0000000
--- a/src/docs/chapter/user/55_JavaAPI/00_JavaAPI.adoc
+++ /dev/null
@@ -1,2 +0,0 @@
-[[prob-java-api]]
-= ProB Java API
diff --git a/src/docs/chapter/user/60_JavaAPI/00_section_header.adoc b/src/docs/chapter/user/60_JavaAPI/00_section_header.adoc
new file mode 100644
index 0000000..43a5344
--- /dev/null
+++ b/src/docs/chapter/user/60_JavaAPI/00_section_header.adoc
@@ -0,0 +1,4 @@
+
+[[prob2-java-api]]
+= ProB 2.0 Java API
+:leveloffset: +1
diff --git a/src/docs/chapter/user/55_JavaAPI/01_ProB_Java_API.adoc b/src/docs/chapter/user/60_JavaAPI/01_ProB_Java_API.adoc
similarity index 94%
rename from src/docs/chapter/user/55_JavaAPI/01_ProB_Java_API.adoc
rename to src/docs/chapter/user/60_JavaAPI/01_ProB_Java_API.adoc
index 1e43835..b17f1cc 100644
--- a/src/docs/chapter/user/55_JavaAPI/01_ProB_Java_API.adoc
+++ b/src/docs/chapter/user/60_JavaAPI/01_ProB_Java_API.adoc
@@ -1,14 +1,15 @@
+
[[general-java-api]]
-== General
+= General
[[prob-java-api-documentation]]
-=== Documentation
+== Documentation
* <<prob-java-api-tutorial,Tutorial>>
* https://www3.hhu.de/stups/handbook/prob2/handbook.html[Developer Manual]
-=== Additional Material
+== Additional Material
* <<prob2.0-development,ProB 2.0 Development>>
* https://github.com/bendisposto/prob2_tooling_template[ProB 2.0 Tooling
@@ -26,7 +27,7 @@ Tutorial Presentation>>
* <<prob-2.0-within-rodin-and-a-html-visualization-example,ProB 2.0
within Rodin and a HTML Visualization Example>>
-=== Download
+== Download
Nightly builds of ProB 2 for Rodin 3 can be obtained from within Rodin
using the update site
diff --git a/src/docs/chapter/user/55_JavaAPI/02_ProB_Java_API_Tutorial.adoc b/src/docs/chapter/user/60_JavaAPI/02_ProB_Java_API_Tutorial.adoc
similarity index 94%
rename from src/docs/chapter/user/55_JavaAPI/02_ProB_Java_API_Tutorial.adoc
rename to src/docs/chapter/user/60_JavaAPI/02_ProB_Java_API_Tutorial.adoc
index 2241dc7..ef3480a 100644
--- a/src/docs/chapter/user/55_JavaAPI/02_ProB_Java_API_Tutorial.adoc
+++ b/src/docs/chapter/user/60_JavaAPI/02_ProB_Java_API_Tutorial.adoc
@@ -1,5 +1,6 @@
+
[[prob-java-api-tutorial]]
-== ProB Java API Tutorial
+= ProB Java API Tutorial
ProB 2.0 is currently experimental. This means that the implementation
may change during the course of development. However, we have reached
@@ -8,7 +9,7 @@ certain level of stability. Therefore, we are writing this tutorial to
explain what those features are.
[[how-to-get-started-developing-with-prob-2.0]]
-=== How to get started developing with ProB 2.0
+== How to get started developing with ProB 2.0
The source code for ProB 2.0 is available via GitHub. Click
https://github.com/bendisposto/prob2[here] to view the prob2 repository.
@@ -20,7 +21,7 @@ can view the features that we are currently working on and can submit
new feature requests.
[[how-to-open-the-groovy-shell]]
-=== How to open the Groovy Shell
+== How to open the Groovy Shell
The ProB Groovy shell is available in the Eclipse application. To open
it, select
@@ -34,7 +35,7 @@ Then select
and hit `ok`.
[[open-the-prob-api-from-sourcejar-file]]
-=== Open the ProB API from Source/JAR file
+== Open the ProB API from Source/JAR file
In order to access the console from source or from a JAR file, start the
application with the parameters -s (short for --shell) and -local (which
@@ -46,10 +47,10 @@ can then be accessed at the following address:
localhost:PORTNR/sessions/GroovyConsoleSession
[[how-to-load-a-model]]
-=== How to load a model
+== How to load a model
[[java-api-classical-b]]
-==== Classical B
+=== Classical B
You can load a Classical B model into the groovy console using the `api`
variable that is available. There is a method `b_load` that is available
@@ -60,7 +61,7 @@ to load Classical B models. For example:
will load example.mch into the variable `m`.
[[java-api-event-b]]
-==== Event B
+=== Event B
To load an Event B model into ProB, right click on the model and select
@@ -73,12 +74,12 @@ command in the Api object. The eventb_load command accepts .bcm and .bcc
files.
[[how-to-animate-models]]
-=== How to animate models
+== How to animate models
The Trace abstraction is available to carry out animations.
[[in-the-console]]
-==== In The Console
+=== In The Console
There are several different ways that a new transition can be added to
the current trace. The most important thing to remember is that each
@@ -141,7 +142,7 @@ Move forwards:
`t = t.forward()`
[[in-the-ui]]
-==== In The UI
+=== In The UI
In order to animate a loaded model in the UI, double-click on an enabled
event in the `Events` view. Then, the resulting trace will automatically
@@ -150,7 +151,7 @@ move backwards and forwards in the trace, use the buttons in the upper
right hand corner of the `Events` view.
[[how-to-switch-from-ui-to-groovy-console]]
-=== How to switch from UI to groovy console
+== How to switch from UI to groovy console
There is an easy way to switch from the UI to the groovy console and
back. It all happens using the "animations" global variable in the
@@ -158,7 +159,7 @@ groovy console. What is important to remember, is that in this case,
there is no distinction between an animation and a trace.
[[from-ui-to-console]]
-==== From UI to Console
+=== From UI to Console
In the UI, switch to the `Current Animations` view. Here you can view
the different animations that are available. If the desired animation is
@@ -172,7 +173,7 @@ into the groovy console and the current animation will be loaded into
the variable `x`.
[[from-the-console-to-the-ui]]
-==== From the Console to the UI
+=== From the Console to the UI
If you have a trace saved into variable `trace_0` in the groovy console,
you can easily add it to the UI. Simply type
@@ -183,7 +184,7 @@ into the groovy console and the trace will automatically be added to the
list of current animations and all of the views will be updated.
[[how-to-carry-out-evaluations]]
-=== How to carry out evaluations
+== How to carry out evaluations
It is very simple to evaluate strings in the groovy console. There is a
build in eval method in both the Trace and the StateSpace. In the trace,
@@ -229,7 +230,7 @@ extract a StateId from a StateSpace, you can use the notation
StateId that you want to view.
[[how-to-convert-between-the-main-abstractions]]
-=== How to convert between the main abstractions
+== How to convert between the main abstractions
There is a connection between all of the main abstractions. You can
easily convert between them by using the `as` operator.
@@ -266,7 +267,7 @@ StateSpace or Model to a Trace, a new trace from the root state is
created.
[[how-to-save-a-trace]]
-=== How to save a trace
+== How to save a trace
ProB currently supports a mechanism to save a trace in a script so that
the same trace can be recreated. We are currently working on some
@@ -304,7 +305,7 @@ TraceConverter
`trace = TraceConverter.restore(modelForThisTrace,"/pathToFile/fileName.xml")`
[[how-to-run-a-groovy-script]]
-=== How to run a groovy script
+== How to run a groovy script
You can use the build in `run` command to run a groovy script. Simply
type
@@ -314,7 +315,7 @@ type
into the console.
[[how-to-animate-with-only-the-statespace-abstraction]]
-=== How to animate with only the StateSpace abstraction
+== How to animate with only the StateSpace abstraction
It is also possible to carry out animations without using a trace
object.
@@ -335,7 +336,7 @@ the event. If there are no parameters, the predicate "TRUE = TRUE"
will automatically be added.
[[how-to-use-a-different-probcli-binary-for-prob2]]
-=== How to use a different probcli binary for ProB2
+== How to use a different probcli binary for ProB2
You need to start ProB2 or the respective Java application with:
diff --git a/src/docs/chapter/user/55_JavaAPI/10_Programmatic_Abstractions_in_the_ProB_2.0_API.adoc b/src/docs/chapter/user/60_JavaAPI/10_Programmatic_Abstractions_in_the_ProB_2.0_API.adoc
similarity index 96%
rename from src/docs/chapter/user/55_JavaAPI/10_Programmatic_Abstractions_in_the_ProB_2.0_API.adoc
rename to src/docs/chapter/user/60_JavaAPI/10_Programmatic_Abstractions_in_the_ProB_2.0_API.adoc
index ba955b8..fcca192 100644
--- a/src/docs/chapter/user/55_JavaAPI/10_Programmatic_Abstractions_in_the_ProB_2.0_API.adoc
+++ b/src/docs/chapter/user/60_JavaAPI/10_Programmatic_Abstractions_in_the_ProB_2.0_API.adoc
@@ -1,11 +1,12 @@
+
[[programmatic-abstractions-in-prob-api]]
-== Programmatic Abstraction in the ProB 2.0 API
+= Programmatic Abstraction in the ProB 2.0 API
[[overview-programmatic-abstractions-in-prob-api]]
-=== Overview
+== Overview
[[background]]
-==== Background
+=== Background
The original ProB plug-in for Rodin introduced one basic abstraction:
developers can create Java commands specifying calculations that are to
@@ -14,7 +15,7 @@ can then be interpreted and manipulated by the developer. Each Java
command corresponds to one prolog instruction in the ProB kernel.
[[current-implementation]]
-==== Current Implementation
+=== Current Implementation
We have maintained the abstractions of the commands in order to
communicate with the ProB kernel. However, as we were considering how
@@ -24,7 +25,7 @@ Therefore, we created the programmatic abstractions that will be
described in the following sections.
[[java-api-model]]
-=== Model
+== Model
The Model is an abstraction that provides static information about the
current model that is being animated or checked. For Classical B and
@@ -45,7 +46,7 @@ information about the model. TLA+ specifications can be represented in
the API as Classical B models.
[[java-api-statespace]]
-=== StateSpace
+== StateSpace
There is a one-to-one relationship between a StateSpace and a model. The
StateSpace is the corresponding label transition system for a particular
@@ -65,7 +66,7 @@ not accessed for a given period of time, the garbage collector can clean
them up.
[[java-api-trace]]
-=== Trace
+== Trace
For some tools, the StateSpace abstraction may be sufficient. But when
it comes to animation and the concept of a "current state", a further
diff --git a/src/docs/chapter/user/55_JavaAPI/20_Rodin_User_and_Developer_Workshop_2013_-_Tutorial.adoc b/src/docs/chapter/user/60_JavaAPI/20_Rodin_User_and_Developer_Workshop_2013_-_Tutorial.adoc
similarity index 98%
rename from src/docs/chapter/user/55_JavaAPI/20_Rodin_User_and_Developer_Workshop_2013_-_Tutorial.adoc
rename to src/docs/chapter/user/60_JavaAPI/20_Rodin_User_and_Developer_Workshop_2013_-_Tutorial.adoc
index 48f121b..9ac986f 100644
--- a/src/docs/chapter/user/55_JavaAPI/20_Rodin_User_and_Developer_Workshop_2013_-_Tutorial.adoc
+++ b/src/docs/chapter/user/60_JavaAPI/20_Rodin_User_and_Developer_Workshop_2013_-_Tutorial.adoc
@@ -1,5 +1,6 @@
+
[[rodin-user-and-developer-workshop-2013]]
-== Rodin User and Developer Workshop 2013
+= Rodin User and Developer Workshop 2013
Here are the information we have shown you at the tutorial. If you want
to follow this tutorial on your computer you will have to install ProB
@@ -11,7 +12,7 @@ This page was updated in May of 2015 to reflect changes made to the ProB
2.0 API.
[[java-api-setup]]
-=== Setup
+== Setup
You will need a fresh copy of ProB 2.0 installed to your Rodin or the
sourcecode.
@@ -31,7 +32,7 @@ snippets. We assume that you execute all the code snippets. Some of the
snippets rely on the previous execution of other snippets.
[[java-api-preparation]]
-=== Preparation
+== Preparation
1. Import the Scheduler project.
2. Start an animation for Scheduler0
@@ -43,7 +44,7 @@ variable.
space that is associated with `trace`
[[java-api-the-model]]
-=== The Model
+== The Model
A model gives you access to the static properties of a Rodin
development. Such as contexts, machines, constants, variables,
@@ -87,7 +88,7 @@ access to axioms, constants and sets. Let's explore machines.
`ne.getGuards()`
[[java-api-the-state-space]]
-=== The State Space
+== The State Space
The state space represents the whole currently known world for an
@@ -183,7 +184,7 @@ run it at the beginning.
`run new File("myAwesomeScript.groovy")`
[[java-api-traces]]
-=== Traces
+== Traces
A trace represents a path through the state space. It can move forward
and backward through the Trace and can be extended with a new
@@ -231,7 +232,7 @@ decision in the past, the trace drops the future. It behaves in the same
way your browser history does.
[[java-api-evaluation]]
-=== Evaluation
+== Evaluation
Evaluation is done by passing an instance of the interface IEvalElement
to an evaluator. Each formalism has its own descendant of IEvalElement.
@@ -304,7 +305,7 @@ of predicates into a conjunction. In Groovy collect means map and inject
means reduce.
[[java-api-constraint-solver]]
-=== Constraint solver
+== Constraint solver
*Evaluation is fine, but can I use ProB's solver?*
@@ -349,7 +350,7 @@ cbc_solve(s, i & i.implies(g))
....
[[java-api-notification-and-ui-access]]
-=== Notification and UI Access
+== Notification and UI Access
Clients can register themself to receive a notification if an animation
step occured, new states were discovered or the model has changed. The
@@ -382,6 +383,6 @@ in the future to something more meaningful, e.g., loader.
`animations.addNewAnimation(t)`
[[java-api-additional-resources]]
-=== Additional Resources
+== Additional Resources
Further information can be found in the ProB Developer_Manual.
diff --git a/src/docs/chapter/user/60_JavaAPI/ZZ_section_footer.adoc b/src/docs/chapter/user/60_JavaAPI/ZZ_section_footer.adoc
new file mode 100644
index 0000000..909c09e
--- /dev/null
+++ b/src/docs/chapter/user/60_JavaAPI/ZZ_section_footer.adoc
@@ -0,0 +1,2 @@
+
+:leveloffset: -1
diff --git a/src/docs/chapter/developer/10_java_api/00_section_header.adoc b/src/docs/chapter/user/65_Java_2-0_API/00_section_header.adoc
similarity index 98%
rename from src/docs/chapter/developer/10_java_api/00_section_header.adoc
rename to src/docs/chapter/user/65_Java_2-0_API/00_section_header.adoc
index 572c682..ec4a27c 100644
--- a/src/docs/chapter/developer/10_java_api/00_section_header.adoc
+++ b/src/docs/chapter/user/65_Java_2-0_API/00_section_header.adoc
@@ -1,3 +1,4 @@
+
[[developer-prob-java-api]]
= ProB 2.0 Java API
:leveloffset: +1
diff --git a/src/docs/chapter/developer/10_java_api/01_introduction.adoc b/src/docs/chapter/user/65_Java_2-0_API/01_introduction.adoc
similarity index 99%
rename from src/docs/chapter/developer/10_java_api/01_introduction.adoc
rename to src/docs/chapter/user/65_Java_2-0_API/01_introduction.adoc
index 3230098..0e99321 100644
--- a/src/docs/chapter/developer/10_java_api/01_introduction.adoc
+++ b/src/docs/chapter/user/65_Java_2-0_API/01_introduction.adoc
@@ -1,3 +1,4 @@
+
[[developer-introduction]]
= Introduction
diff --git a/src/docs/chapter/developer/10_java_api/02_architecture.adoc b/src/docs/chapter/user/65_Java_2-0_API/02_architecture.adoc
similarity index 98%
rename from src/docs/chapter/developer/10_java_api/02_architecture.adoc
rename to src/docs/chapter/user/65_Java_2-0_API/02_architecture.adoc
index db0d731..b43f74b 100644
--- a/src/docs/chapter/developer/10_java_api/02_architecture.adoc
+++ b/src/docs/chapter/user/65_Java_2-0_API/02_architecture.adoc
@@ -1,3 +1,5 @@
+
+[[developer-architecture]]
= Architecture
In this chapter we will give an overview of the tool's architecture. First we will explain the base components and then we will explain how these components interact with each other.
diff --git a/src/docs/chapter/developer/10_java_api/03_installation.adoc b/src/docs/chapter/user/65_Java_2-0_API/03_installation.adoc
similarity index 96%
rename from src/docs/chapter/developer/10_java_api/03_installation.adoc
rename to src/docs/chapter/user/65_Java_2-0_API/03_installation.adoc
index 243412b..fc215cf 100644
--- a/src/docs/chapter/developer/10_java_api/03_installation.adoc
+++ b/src/docs/chapter/user/65_Java_2-0_API/03_installation.adoc
@@ -1,3 +1,5 @@
+
+[[developer-installation]]
= Installation
You can use the ProB 2.0 archive.
diff --git a/src/docs/chapter/developer/10_java_api/04_lowlevelapi.adoc b/src/docs/chapter/user/65_Java_2-0_API/04_lowlevelapi.adoc
similarity index 99%
rename from src/docs/chapter/developer/10_java_api/04_lowlevelapi.adoc
rename to src/docs/chapter/user/65_Java_2-0_API/04_lowlevelapi.adoc
index 1e22bce..91f0bff 100644
--- a/src/docs/chapter/developer/10_java_api/04_lowlevelapi.adoc
+++ b/src/docs/chapter/user/65_Java_2-0_API/04_lowlevelapi.adoc
@@ -1,3 +1,5 @@
+
+[[developer-low-level-api]]
= Low Level API
The ProB core has two different APIs. One is suited for high level usage and one directly interacts with the Prolog binary. The latter (low level) API is used to extend the functionality of ProB 2.0 and this is the API that we are introducing in this chapter. It is typically only used within the development team because it often requires changing parts of the Prolog kernel. However, it still may be useful to know where one can look for low level features. This is particulary helpful when some of the features are not yet accessible to a higher level API.
diff --git a/src/docs/chapter/developer/10_java_api/05_probcore.adoc b/src/docs/chapter/user/65_Java_2-0_API/05_probcore.adoc
similarity index 99%
rename from src/docs/chapter/developer/10_java_api/05_probcore.adoc
rename to src/docs/chapter/user/65_Java_2-0_API/05_probcore.adoc
index 2ab98c1..9416769 100644
--- a/src/docs/chapter/developer/10_java_api/05_probcore.adoc
+++ b/src/docs/chapter/user/65_Java_2-0_API/05_probcore.adoc
@@ -1,3 +1,5 @@
+
+[[developer-high-level-api]]
= High Level API
We have introduced a high level API in ProB 2.0 which allows much nicer interaction with ProB. Before 2.0, all interaction was done using commands. There were no abstractions that represent typically used concepts such as a model, a state space, or a trace. Together with this high level API, we introduced a scripting interface that makes it very easy to tweak ProB and implement new features. Almost everything in ProB can be manipulated through Groovy scripts. This chapter will introduce the programmatic abstractions now available in ProB 2.0, and will briefly describe their function. Later chapters will cover in greater depth how to use the abstractions. <<animation>> covers the topic of animation, and <<evaluation>> discusses how to evaluate formulas using the API. In the following sections we will introduce the main abstractions that are available in ProB 2.0, that is, the model, state space and trace abstractions.
diff --git a/src/docs/chapter/developer/10_java_api/06_animation.adoc b/src/docs/chapter/user/65_Java_2-0_API/06_animation.adoc
similarity index 99%
rename from src/docs/chapter/developer/10_java_api/06_animation.adoc
rename to src/docs/chapter/user/65_Java_2-0_API/06_animation.adoc
index 0408aaf..2772f42 100644
--- a/src/docs/chapter/developer/10_java_api/06_animation.adoc
+++ b/src/docs/chapter/user/65_Java_2-0_API/06_animation.adoc
@@ -1,3 +1,5 @@
+
+[[developer-animation]]
= Animation
It is possible for the user to perform animation manually using the state and transition abstractions, or to use the trace abstraction which allows the user access to previously executed transitions, and the ability to move within the trace. This chapter will describe in detail all of the different ways that it is possible to perform animation using the provided abstractions.
diff --git a/src/docs/chapter/developer/10_java_api/07_evaluation.adoc b/src/docs/chapter/user/65_Java_2-0_API/07_evaluation.adoc
similarity index 99%
rename from src/docs/chapter/developer/10_java_api/07_evaluation.adoc
rename to src/docs/chapter/user/65_Java_2-0_API/07_evaluation.adoc
index 1eb2e43..8c6af3f 100644
--- a/src/docs/chapter/developer/10_java_api/07_evaluation.adoc
+++ b/src/docs/chapter/user/65_Java_2-0_API/07_evaluation.adoc
@@ -1,3 +1,5 @@
+
+[[developer-evaluation-and-constraint-solving]]
= Evaluation and Constraint Solving
This chapter will demonstrate how we evaluate formulas in the context of a formal model. It also demonstrates how we can use ProB's constraint solver.
diff --git a/src/docs/chapter/developer/10_java_api/08_cosimulation.adoc b/src/docs/chapter/user/65_Java_2-0_API/08_cosimulation.adoc
similarity index 97%
rename from src/docs/chapter/developer/10_java_api/08_cosimulation.adoc
rename to src/docs/chapter/user/65_Java_2-0_API/08_cosimulation.adoc
index 725dc60..6c08fd7 100644
--- a/src/docs/chapter/developer/10_java_api/08_cosimulation.adoc
+++ b/src/docs/chapter/user/65_Java_2-0_API/08_cosimulation.adoc
@@ -1,3 +1,5 @@
+
+[[co-simulation]]
= Co-Simulation
ProB 2.0 contains some classes for cosimulating discrete models specified in one of the formalisms that are supported by ProB, and continuous models that are implemented using the https://fmi-standard.org/[functional mockup interface] standard. A so called functional mockup unit (FMU) can, for example, be created in C using the FMI SDK or exported from third party tools such as Dymola. The framework is built on top of https://ptolemy.berkeley.edu/java/jfmi//[JFMI] from the Ptolemy Project. In fact, we only added a thin wrapper on top of the JFMI library.
diff --git a/src/docs/chapter/developer/10_java_api/09_dependencyinjection.adoc b/src/docs/chapter/user/65_Java_2-0_API/09_dependencyinjection.adoc
similarity index 99%
rename from src/docs/chapter/developer/10_java_api/09_dependencyinjection.adoc
rename to src/docs/chapter/user/65_Java_2-0_API/09_dependencyinjection.adoc
index dec1dbd..3ed8328 100644
--- a/src/docs/chapter/developer/10_java_api/09_dependencyinjection.adoc
+++ b/src/docs/chapter/user/65_Java_2-0_API/09_dependencyinjection.adoc
@@ -1,3 +1,5 @@
+
+[[dependency-injection]]
= Dependency Injection
We have decided to use the Guice framework for dependency injection. Although this is just an implementation detail it is important to get a basic understanding of how it works and why we use it in order to build tools on top of ProB 2.0. A more complete introduction to dependency injection and the Guice framework can be found in cite:[Prasanna:2009:DI:1795686] and https://github.com/google/guice[the Guice website].
diff --git a/src/docs/chapter/user/65_Java_2-0_API/ZZ_section_footer.adoc b/src/docs/chapter/user/65_Java_2-0_API/ZZ_section_footer.adoc
new file mode 100644
index 0000000..909c09e
--- /dev/null
+++ b/src/docs/chapter/user/65_Java_2-0_API/ZZ_section_footer.adoc
@@ -0,0 +1,2 @@
+
+:leveloffset: -1
diff --git a/src/docs/chapter/user/70_TclTk/00_section_header.adoc b/src/docs/chapter/user/70_TclTk/00_section_header.adoc
new file mode 100644
index 0000000..c68e1ae
--- /dev/null
+++ b/src/docs/chapter/user/70_TclTk/00_section_header.adoc
@@ -0,0 +1,4 @@
+
+[[tcltk]]
+= Tcl/Tk
+:leveloffset: +1
diff --git a/src/docs/chapter/developer/30_tcltk/Tk_Architecture.adoc b/src/docs/chapter/user/70_TclTk/Tk_Architecture.adoc
similarity index 100%
rename from src/docs/chapter/developer/30_tcltk/Tk_Architecture.adoc
rename to src/docs/chapter/user/70_TclTk/Tk_Architecture.adoc
diff --git a/src/docs/chapter/user/70_TclTk/ZZ_section_footer.adoc b/src/docs/chapter/user/70_TclTk/ZZ_section_footer.adoc
new file mode 100644
index 0000000..909c09e
--- /dev/null
+++ b/src/docs/chapter/user/70_TclTk/ZZ_section_footer.adoc
@@ -0,0 +1,2 @@
+
+:leveloffset: -1
diff --git a/src/docs/chapter/user/YZ_Tutorials/00_section_header.adoc b/src/docs/chapter/user/YZ_Tutorials/00_section_header.adoc
new file mode 100644
index 0000000..0afe68c
--- /dev/null
+++ b/src/docs/chapter/user/YZ_Tutorials/00_section_header.adoc
@@ -0,0 +1,4 @@
+
+[[tutorials]]
+= Tutorials
+:leveloffset: +1
diff --git a/src/docs/chapter/user/10_General/Tutorial_Animation_Tips.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Animation_Tips.adoc
similarity index 93%
rename from src/docs/chapter/user/10_General/Tutorial_Animation_Tips.adoc
rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Animation_Tips.adoc
index e2eca00..f0d8808 100644
--- a/src/docs/chapter/user/10_General/Tutorial_Animation_Tips.adoc
+++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Animation_Tips.adoc
@@ -1,12 +1,13 @@
+
[[tutorial-animation-tips]]
-== Tutorial Animation Tips
+= Tutorial Animation Tips
Make sure you have the Lift.mch model from the first part of the
tutorial: <<tutorial-first-step,Starting ProB and first animation
steps>>.
[[operation-with-many-solutions-for-the-parameters]]
-=== Operation with many solutions for the parameters
+== Operation with many solutions for the parameters
Add the following operation to the Lift model:
@@ -27,7 +28,7 @@ all possible parameter values for the operations were computed.
There are several solutions to overcome this.
[[increasing-max_operations]]
-==== Increasing MAX_OPERATIONS
+=== Increasing MAX_OPERATIONS
First, you could increase the "MAX_OPERATIONS" preference of ProB by
selecting the "Animation Preferences" command in the _Preferences_
@@ -41,7 +42,7 @@ the B machine.
image::ProB_Lift_OpPane_WithJump101.png[]
[[executing-an-operation-by-predicate]]
-==== Executing an Operation by Predicate
+=== Executing an Operation by Predicate
The alternative is to provide the parameter value for `level` yourself.
For this, select the "Execute an Operation..." command in the _Animate_
@@ -71,7 +72,7 @@ value `98` for level. When there are multiple solutions, ProB will only
execute the operation for the first solution found.
[[using-random-enumeration]]
-==== Using Random enumeration
+=== Using Random enumeration
You can also tell ProB to try and perform random enumerations. This
feature is available in ProB 1.5.0 or newer. You add the following lines
@@ -87,10 +88,10 @@ you should see a picture similar to the following one:
image::ProB_Lift_Randomise.png[]
[[using-constraint-based-validation-techniques]]
-==== Using Constraint-Based Validation Techniques
+=== Using Constraint-Based Validation Techniques
[[find-sequence]]
-===== Find Sequence
+==== Find Sequence
You can also use the constraint solver to construct sequences which are
of interest to you. Let us add the following operation to the lift
@@ -119,7 +120,7 @@ it:
image::FindSequenceResult.png[]
[[constraint-based-model-based-testing]]
-===== Constraint-Based Model-Based Testing
+==== Constraint-Based Model-Based Testing
Alternatively, you could for example use the constraint-based test-case
generator to find for every operation the shortest trace that enables
diff --git a/src/docs/chapter/user/30_OtherLanguages/CSP/04_Tutorial_CSP_First_Step.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_CSP_First_Step.adoc
similarity index 96%
rename from src/docs/chapter/user/30_OtherLanguages/CSP/04_Tutorial_CSP_First_Step.adoc
rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_CSP_First_Step.adoc
index e500f9d..99becf3 100644
--- a/src/docs/chapter/user/30_OtherLanguages/CSP/04_Tutorial_CSP_First_Step.adoc
+++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_CSP_First_Step.adoc
@@ -1,12 +1,11 @@
-
[[tutorial-csp-first-step]]
-=== Tutorial CSP First Step
+= Tutorial CSP First Step
[Category:User Manual]
[[startup]]
-==== Startup
+== Startup
Start off by installing the standalone Tcl/Tk version of ProB. Follow
the instructions in <<installation,Installation>>. Start ProB by
@@ -14,7 +13,7 @@ double-clicking on `ProBWin` (for Windows users), or by launching
`StartProB.sh` from a Terminal (for Linux and Mac users).
[[loading-a-first-csp-specification]]
-==== Loading a first CSP specification
+== Loading a first CSP specification
Use the "Open..." command in the _File_ menu and then navigate to
the "Examples" directory that came with your ProB installation. Inside
@@ -24,7 +23,7 @@ ProB window should now look as follows:
image::ProB_BusesAfterLoad.png[]
[[first-steps-in-animation-csp]]
-==== First Steps in Animation
+== First Steps in Animation
We have now loaded a first simple CSP model. Let us look at the contents
of the ProB window (ignoring the menu bar).
@@ -71,7 +70,7 @@ source locations). The source highlighting should look as follows:
image::ProB_CSPAfterBoardSingleClick.png[]
[[first-steps-in-model-checking]]
-==== First Steps in Model Checking
+== First Steps in Model Checking
You can use the model checker to search for certain errors. Execute the
"Model Check..." command in the _Verify_ menu. The following dialog
@@ -91,7 +90,7 @@ insert the counter-example into the history as follows:
image::ProB_CSPAfterModelCheck.png[]
[[error-highlighting]]
-==== Error Highlighting
+== Error Highlighting
Now edit the definition of the BUS37 process and add an illegal output
of value 1 on the alight37B channel:
@@ -116,7 +115,7 @@ error location in the source as follows:
image::ProB_CSPAfterModelCheck2.png[]
[[other-features]]
-==== Other Features
+== Other Features
You can check more sophisticated temporal properties using the LTL model
checker of ProB; see the <<ltl-model-checking,corresponding part of
diff --git a/src/docs/chapter/user/40_AdvancedFeatures/10_Tutorials/Tutorial_Co-Simulation.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Co-Simulation.adoc
similarity index 96%
rename from src/docs/chapter/user/40_AdvancedFeatures/10_Tutorials/Tutorial_Co-Simulation.adoc
rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Co-Simulation.adoc
index e354cdc..d61c5ad 100644
--- a/src/docs/chapter/user/40_AdvancedFeatures/10_Tutorials/Tutorial_Co-Simulation.adoc
+++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Co-Simulation.adoc
@@ -1,10 +1,11 @@
+
[[tutorial-co-simulation]]
-== Tutorial Co-Simulation
+= Tutorial Co-Simulation
You can create Co-Simulations using FMI with ProB.
[[overview-tutorial-co-simulation]]
-=== Overview
+== Overview
The ProB 2.0 Java API contains some classes for cosimulating discrete
models specified in one of the formalisms that are supported by ProB,
diff --git a/src/docs/chapter/user/20_Validation/MC/Tutorial_Complete_Model_Checking.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Complete_Model_Checking.adoc
similarity index 97%
rename from src/docs/chapter/user/20_Validation/MC/Tutorial_Complete_Model_Checking.adoc
rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Complete_Model_Checking.adoc
index cea4ec9..5095a17 100644
--- a/src/docs/chapter/user/20_Validation/MC/Tutorial_Complete_Model_Checking.adoc
+++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Complete_Model_Checking.adoc
@@ -1,5 +1,6 @@
+
[[tutorial-complete-model-checking]]
-== Tutorial Complete Model Checking
+= Tutorial Complete Model Checking
We assume that you have completed
<<tutorial-first-model-checking,Tutorial First Model Checking>>.
@@ -33,7 +34,7 @@ will compute at most 5 possible ways to execute any given operation
(i.e., Increase and Reset in this case). We return to this issue below.
[[successful-model-checking]]
-=== Successful Model Checking
+== Successful Model Checking
Now select the "Model Check..." command in the _Verify_ menu which
brings up the model checking dialog box:
@@ -55,7 +56,7 @@ about interpreting a completed model check. Below we examine several
issues that have to be considered.
[[computing-all-transitions]]
-=== Computing All Transitions
+== Computing All Transitions
Let us now adapt the above B machine by changing the DEFINITION of MAX
to 6. Now repeat the model checking exercise above. This time ProB will
@@ -95,7 +96,7 @@ a counter example:
image::ProBSimpleCounterForMC_InvViol.png[]
[[tutorial-deferred-sets]]
-=== Deferred Sets
+== Deferred Sets
Let us now use the following simple machine:
@@ -155,7 +156,7 @@ SETS ID={id1,id2,id3,id4,id5}
....
[[infinite-types]]
-=== Infinite Types
+== Infinite Types
It could be that your B machine makes use of the mathematical integers
(`INTEGER`) or infinite subsets thereof (`NATURAL`, `NATURAL1`). Note
@@ -176,7 +177,7 @@ it. This information is not yet fed back to the graphical user interface
(but we are working on it).
[[model-checking-and-proof]]
-=== Model Checking and Proof
+== Model Checking and Proof
Finally, even if ProB was able to successfully check the entire state
space of your model, this does not imply that you can prove your machine
diff --git a/src/docs/chapter/user/11_BLanguage/WD/10_Tutorial_Debugging_Well-Definedness_and_Transition_Errors.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Debugging_Well-Definedness_and_Transition_Errors.adoc
similarity index 96%
rename from src/docs/chapter/user/11_BLanguage/WD/10_Tutorial_Debugging_Well-Definedness_and_Transition_Errors.adoc
rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Debugging_Well-Definedness_and_Transition_Errors.adoc
index 1187533..d0eac52 100644
--- a/src/docs/chapter/user/11_BLanguage/WD/10_Tutorial_Debugging_Well-Definedness_and_Transition_Errors.adoc
+++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Debugging_Well-Definedness_and_Transition_Errors.adoc
@@ -1,5 +1,6 @@
+
[[tutorial-debugging-well-definedness-and-transition-errors]]
-== Tutorial Debugging Well-Definedness and Transition Errors
+= Tutorial Debugging Well-Definedness and Transition Errors
We assume that you have grasped the way that ProB setups up the initial
states of a B machine as outlined in
@@ -10,7 +11,7 @@ Understanding the Complexity of B Animation>>. You may also want to have
a look at the explanation of
<<well-definedness-checking,well-definedness in B>>.
-=== A simple example
+== A simple example
Let us use the following B machine as starting point:
diff --git a/src/docs/chapter/user/20_Validation/MC/Tutorial_Directed_Model_Checking.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Directed_Model_Checking.adoc
similarity index 98%
rename from src/docs/chapter/user/20_Validation/MC/Tutorial_Directed_Model_Checking.adoc
rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Directed_Model_Checking.adoc
index 513fc0e..fdd8745 100644
--- a/src/docs/chapter/user/20_Validation/MC/Tutorial_Directed_Model_Checking.adoc
+++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Directed_Model_Checking.adoc
@@ -1,5 +1,6 @@
+
[[tutorial-directed-model-checking]]
-== Tutorial Directed Model Checking
+= Tutorial Directed Model Checking
We assume that you have completed
<<tutorial-first-model-checking,Tutorial First Model Checking>> and
@@ -102,7 +103,7 @@ Below we show the output of the above command for the various choices of
.
[[breadth-first]]
-=== Breadth-First
+== Breadth-First
`$ probcli phonebook7.mch -p MAX_OPERATIONS 99 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode bf`
@@ -115,7 +116,7 @@ requirements can be very large and it can take very long to find long
counter examples.
[[depth-first]]
-=== Depth-First
+== Depth-First
`$ probcli phonebook7.mch -p MAX_OPERATIONS 99 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode df`
@@ -132,7 +133,7 @@ and possibly hard to understand for the user. The next search strategy,
tries to combine the advantages of breadth-first and depth-first search.
[[mixed-dfbf]]
-=== Mixed DF/BF
+== Mixed DF/BF
The mixed search strategy, tries to combine the advantages of
breadth-first and depth-first search. It is the default setting for
@@ -156,7 +157,7 @@ It is interesting to compare this result with the random search
strategy, which we show next.
[[random]]
-=== Random
+== Random
`$ probcli phonebook7.mch -p MAX_OPERATIONS 99 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode random`
@@ -170,7 +171,7 @@ Compared to the `mixed` option one can notice that the mixed option has
more of a tendency to explore certain branches in depth.
[[hash]]
-=== Hash
+== Hash
`$ probcli phonebook7.mch -p MAX_OPERATIONS 99 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode hash`
@@ -181,7 +182,7 @@ the same result, as the hash value of the states do not change from one
run of ProB to another.
[[out-degree]]
-=== Out-Degree
+== Out-Degree
`$ probcli phonebook7.mch -p MAX_OPERATIONS 99 -mc 10 -spdot out.dot -p DOT_LEAVES FALSE -mc_mode dlk`
@@ -194,7 +195,7 @@ and delete). Note: here it is important to set the `MAX_OPERATIONS` high
enough, otherwise the resulting state space could be different.
[[more-examples]]
-=== More examples
+== More examples
A further illustration of directed model checking can be found in our
<<blocks-world-directed-model-checking,"Blocks World" example>>.
diff --git a/src/docs/chapter/user/40_AdvancedFeatures/10_Tutorials/Tutorial_Disprover.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Disprover.adoc
similarity index 95%
rename from src/docs/chapter/user/40_AdvancedFeatures/10_Tutorials/Tutorial_Disprover.adoc
rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Disprover.adoc
index 4ab91a9..9c7a062 100644
--- a/src/docs/chapter/user/40_AdvancedFeatures/10_Tutorials/Tutorial_Disprover.adoc
+++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Disprover.adoc
@@ -1,8 +1,9 @@
+
[[tutorial-disprover]]
-== Tutorial Disprover
+= Tutorial Disprover
[[warning]]
-=== WARNING
+== WARNING
We believe the Disprover to be useful. The disprover plugin is currently
still experimental when used as a prover. Please keep in mind, that you
@@ -10,7 +11,7 @@ might run into some rough edges or even get wrong results (please inform
us about any issues).
[[introduction-tutorial-disprover]]
-=== Introduction
+== Introduction
The ProB Disprover plugin for RODIN utilizes the ProB animator and model
checker to automatically find counterexamples or proofs for a given
@@ -28,14 +29,14 @@ proof. See https://www3.hhu.de/stups/downloads/pdf/disprover_eval.pdf[the
paper describing the disprover as a prover] for more details.
[[installation-tutorial-disprover]]
-=== Installation
+== Installation
The ProB Disprover is currently only available through the ProB Nightly
Build Update Site
(http://nightly.cobra.cs.uni-duesseldorf.de/rodin/updatesite/).
[[how-to-use-it]]
-=== How to use it
+== How to use it
image::Disprover-all.png[]
@@ -46,7 +47,7 @@ the tool bar alongside the other provers:
image::Disprover_proof_control.png[]
[[how-it-works]]
-=== How it works
+== How it works
Upon selecting the Disprover, it builds a formula from the Hypotheses
and the negated Goal. The ProB model checker then tries to find a model
diff --git a/src/docs/chapter/user/20_Validation/CBC/30_Tutorial_Enabling_Analysis.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Enabling_Analysis.adoc
similarity index 99%
rename from src/docs/chapter/user/20_Validation/CBC/30_Tutorial_Enabling_Analysis.adoc
rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Enabling_Analysis.adoc
index 2a327d0..936e414 100644
--- a/src/docs/chapter/user/20_Validation/CBC/30_Tutorial_Enabling_Analysis.adoc
+++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Enabling_Analysis.adoc
@@ -1,5 +1,6 @@
+
[[tutorial-enabling-analysis]]
-== Tutorial Enabling Analysis
+= Tutorial Enabling Analysis
The B-method and in particular its successor Event-B are methodologies
for formal development and verification of systems. In Event-B, a
@@ -25,7 +26,7 @@ a table or by means of a graph. For simplicity, we will concentrate
mainly on B and use the terminology of the formalism.
[[enabling-relations]]
-=== Enabling Relations
+== Enabling Relations
What we want to find out is how the operations influence each other
within a B model. In other words, for each pair (op1, op2) of operations
@@ -205,7 +206,7 @@ and deduce some properties. For example, we can clearly see that `Op4`
cannot occur after the execution of another operation.
[[summary-of-the-enabling-relations]]
-=== Summary of the Enabling Relations
+== Summary of the Enabling Relations
In the following, we summarize most of the enabling relations that we
think can provide a useful feedback to the user. For each of the
@@ -273,7 +274,7 @@ image::PossibleDisableExample.png[]
image::InfeasibleExample.png[]
[[performing-enabling-analysis-within-prob]]
-=== Performing Enabling Analysis within ProB
+== Performing Enabling Analysis within ProB
The enabling analysis has been implemented in the ProB toolset. The
computation of the enabling relations is based on syntactic and
@@ -387,4 +388,4 @@ whether a single event is in principle possible (given the invariant):
$ probcli file.mch -feasibility_analysis_csv FILE
....
-=== References and Footnotes
+== References and Footnotes
diff --git a/src/docs/chapter/user/20_Validation/MC/Tutorial_First_Model_Checking.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_First_Model_Checking.adoc
similarity index 97%
rename from src/docs/chapter/user/20_Validation/MC/Tutorial_First_Model_Checking.adoc
rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_First_Model_Checking.adoc
index 0b57744..8018e4b 100644
--- a/src/docs/chapter/user/20_Validation/MC/Tutorial_First_Model_Checking.adoc
+++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_First_Model_Checking.adoc
@@ -1,5 +1,6 @@
+
[[tutorial-first-model-checking]]
-== Tutorial First Model Checking
+= Tutorial First Model Checking
We assume that you have loaded the "Lift.mch" B machine from the ProB
Examples folder as outlined in <<tutorial-first-step,Tutorial First
@@ -7,7 +8,7 @@ Step>>. There we have also seen how to execute operations on a B machine
by double clicking on the items in the "Enabled Operations" pane.
[[simple-model-checking]]
-=== Simple Model Checking
+== Simple Model Checking
The model checker can be used to systematically execute the operations
and tries to find an erroneous state (e.g., where the invariant is
@@ -39,7 +40,7 @@ sequence that leads to an error or to this error. However, by selecting
the shortest paths are found.)
[[coverage-statistics]]
-=== Coverage Statistics
+== Coverage Statistics
We can obtain some statistics about how many states ProB has explored by
selecting the "Compute Coverage" command in the _Analyse_ menu:
@@ -69,7 +70,7 @@ transitions: we have one initialization, 8 `inc` operations and 8 `dec`
operations.
[[view-statespace]]
-=== View Statespace
+== View Statespace
We can obtain a graphical visualization of the state space explored by
ProB. For this, be sure that you have correctly
diff --git a/src/docs/chapter/user/10_General/Tutorial_First_Step.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_First_Step.adoc
similarity index 97%
rename from src/docs/chapter/user/10_General/Tutorial_First_Step.adoc
rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_First_Step.adoc
index 18720df..a79c151 100644
--- a/src/docs/chapter/user/10_General/Tutorial_First_Step.adoc
+++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_First_Step.adoc
@@ -1,14 +1,15 @@
+
[[tutorial-first-step]]
-== Tutorial First Step
+= Tutorial First Step
[[installation-tutorial-first-step]]
-=== Installation
+== Installation
Start off by installing the standalone Tcl/Tk version of ProB. Follow
the instructions in <<installation,Installation>>.
[[starting-prob-tutorial-first-step]]
-=== Starting ProB
+== Starting ProB
Start ProB by double-clicking on `ProBWin` (for Windows users), or by
launching `StartProB.sh` from a Terminal (for Linux and Mac users).
@@ -32,7 +33,7 @@ Normally, it should look as follows (on Windows):
image::ProBStartTerminal.png[]
[[loading-a-first-b-machine]]
-=== Loading a first B machine
+== Loading a first B machine
Use the "Open..." command in the _File_ menu
@@ -48,7 +49,7 @@ window should now look as follows:
image::ProB_LiftAfterLoad.png[]
[[first-steps-in-animation]]
-=== First Steps in Animation
+== First Steps in Animation
We have now loaded a first simple B model. Let us look at the contents
of the ProB window (ignoring the menu bar).
diff --git a/src/docs/chapter/user/20_Validation/MC/Tutorial_LTL_Counter-example_View.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_LTL_Counter-example_View.adoc
similarity index 98%
rename from src/docs/chapter/user/20_Validation/MC/Tutorial_LTL_Counter-example_View.adoc
rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_LTL_Counter-example_View.adoc
index 5147cc9..10c8f0c 100644
--- a/src/docs/chapter/user/20_Validation/MC/Tutorial_LTL_Counter-example_View.adoc
+++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_LTL_Counter-example_View.adoc
@@ -1,5 +1,6 @@
+
[[tutorial-ltl-counter-example-view]]
-== Tutorial LTL Counter-example View
+= Tutorial LTL Counter-example View
In this tutorial a quick overview will be given describing the LTL
counter-example visualization plug-in in Rodin. The functionality of the
@@ -8,7 +9,7 @@ different properties will be checked that are not satisfied by the
model.
[[ltl-model-checking-and-the-meaning-of-counter-examples]]
-=== LTL Model Checking and the Meaning of Counter-examples
+== LTL Model Checking and the Meaning of Counter-examples
Model checking is a technique for checking in an automatic way whether a
model satisfies a property expressed in formal logic. LTL (standing for
@@ -50,7 +51,7 @@ is a counter-example for each LTL formula latexmath:[$X^{n} (true)$],
with latexmath:[$n\geq 1$].] property, whereas the path in Figure 3
represents usually a counter-example for a safety property.
-=== Visualization of Counter-examples in Rodin
+== Visualization of Counter-examples in Rodin
*Coloring and highlighting nodes in a counter-example*
Each state of a path in the LTL counter-example view is marked by a
@@ -163,7 +164,7 @@ image::LTLViewVisualisation4.png[]
In order to view the visualizations of the sub-formulas, one should
click on one of the states of the source-formula.
-=== Use Case for the LTL Counter-example Viewer
+== Use Case for the LTL Counter-example Viewer
Consider an Event-B model formalizing an algorithm for mutual exclusion
with semaphores for two concurrent processes latexmath:[$P_1$] and
@@ -258,7 +259,7 @@ state ‘p1=wait1’ becomes true. Once a state is encountered where
will hold. This is apparently not fulfilled as in all successor states
_p1_ will not become equal to _crit1_.
-=== Literature Sources
+== Literature Sources
For more detailed information on visualizing counter-examples in the LTL
counter-example view in Rodin refer to footnote:[Andriy Tolstoy,
@@ -272,4 +273,4 @@ Checking_. MIT Press, 2008.].
The Event-B model used in this tutorial can be downloaded from
http://www.stups.uni-duesseldorf.de/~dobrikov/modelchecking/MUTEX.zip[here].
-=== References
+== References
diff --git a/src/docs/chapter/user/20_Validation/CBC/31_Tutorial_Model_Checking,_Proof_and_CBC.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Model_Checking_Proof_and_CBC.adoc
similarity index 97%
rename from src/docs/chapter/user/20_Validation/CBC/31_Tutorial_Model_Checking,_Proof_and_CBC.adoc
rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Model_Checking_Proof_and_CBC.adoc
index fbac058..e35c231 100644
--- a/src/docs/chapter/user/20_Validation/CBC/31_Tutorial_Model_Checking,_Proof_and_CBC.adoc
+++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Model_Checking_Proof_and_CBC.adoc
@@ -1,5 +1,6 @@
+
[[tutorial-model-checking-proof-and-cbc]]
-== Tutorial Model Checking, Proof and CBC
+= Tutorial Model Checking, Proof and CBC
We assume that you have completed
<<tutorial-complete-model-checking,Tutorial Complete Model
@@ -28,7 +29,7 @@ Is this model correct? As you will see, this depends on your point of
view.
[[state-space]]
-=== State Space
+== State Space
If you look purely at the state space of the machine (choose the View
State Space command in the Animate menu) you get the following picture:
@@ -43,7 +44,7 @@ However, you will not be able to prove the system correct using AtelierB
or Rodin.
[[constraint-based-checking-cbc-for-the-invariant]]
-=== Constraint Based Checking (CBC) for the Invariant
+== Constraint Based Checking (CBC) for the Invariant
In addition to model checking, ProB also offers constraint-based
checking (CBC), which is particularly useful when used in conjunction
@@ -118,7 +119,7 @@ operation must preserve the invariant for the state with `counter=65`,
which it does not.
[[how-to-correct-problems-found]]
-=== How to correct problems found
+== How to correct problems found
Below is a small guide on how to correct invariant violations found by
constraint-based checking and model checking.
diff --git a/src/docs/chapter/user/11_BLanguage/30_Tutorial_Modeling_Infinite_Datatypes.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Modeling_Infinite_Datatypes.adoc
similarity index 98%
rename from src/docs/chapter/user/11_BLanguage/30_Tutorial_Modeling_Infinite_Datatypes.adoc
rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Modeling_Infinite_Datatypes.adoc
index 1094ccb..bac81b1 100644
--- a/src/docs/chapter/user/11_BLanguage/30_Tutorial_Modeling_Infinite_Datatypes.adoc
+++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Modeling_Infinite_Datatypes.adoc
@@ -1,7 +1,6 @@
-
[[tutorial-modeling-infinite-datatypes]]
-== Tutorial Modeling Infinite Datatypes
+= Tutorial Modeling Infinite Datatypes
This tutorial describes how to model (and how not to model)
infinite datatypes so that they can be animated with ProB. (You may also
diff --git a/src/docs/chapter/user/30_OtherLanguages/EventB/Tutorial_Rodin_Exporting.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Rodin_Exporting.adoc
similarity index 94%
rename from src/docs/chapter/user/30_OtherLanguages/EventB/Tutorial_Rodin_Exporting.adoc
rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Rodin_Exporting.adoc
index a640e78..5a5dbb4 100644
--- a/src/docs/chapter/user/30_OtherLanguages/EventB/Tutorial_Rodin_Exporting.adoc
+++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Rodin_Exporting.adoc
@@ -1,8 +1,9 @@
+
[[tutorial-rodin-exporting]]
-=== Tutorial Rodin Exporting
+= Tutorial Rodin Exporting
[[introduction-to-tutorial-rodin-exporting]]
-==== Introduction
+== Introduction
Many features of ProB are currently only available in ProB Tcl/Tk or the
<<using-the-command-line-version-of-prob,probcli>> command-line
@@ -10,7 +11,7 @@ version]. Luckily you can export Rodin models for use with those tools.
Below we explain how.
[[exporting-for-prob-classic]]
-==== Exporting for ProB classic
+== Exporting for ProB classic
Start by right clicking (control Click on the Mac) on the machine or
context in the "Event-B Explorer" view you wish to export and select
@@ -23,7 +24,7 @@ default one will do) for the file. The file should have the extension
".eventb" (as suggested by default).
[[loading-an-event-b-project-into-prob-classic]]
-==== Loading an Event-B Project into ProB classic
+== Loading an Event-B Project into ProB classic
You can now use the ".eventb" file directly for probcli. For example,
the following command will perform standard model checking on the file
@@ -57,7 +58,7 @@ into a single ".eventb" project file.
image::ProBRodinLoadedInTclTk.png[]
[[starting-up-prob-classic-directly]]
-==== Starting up ProB Classic Directly
+== Starting up ProB Classic Directly
You can also start up ProB Classic (aka ProB Tcl/Tk) directly, without
first generating an ".eventb" file. For this, start by right clicking
diff --git a/src/docs/chapter/user/30_OtherLanguages/EventB/Tutorial_Rodin_First_Step.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Rodin_First_Step.adoc
similarity index 97%
rename from src/docs/chapter/user/30_OtherLanguages/EventB/Tutorial_Rodin_First_Step.adoc
rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Rodin_First_Step.adoc
index c601db6..c646bb0 100644
--- a/src/docs/chapter/user/30_OtherLanguages/EventB/Tutorial_Rodin_First_Step.adoc
+++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Rodin_First_Step.adoc
@@ -1,8 +1,9 @@
+
[[tutorial-rodin-first-step]]
-=== Tutorial Rodin First Step
+= Tutorial Rodin First Step
[[installation-rodin]]
-==== Installation
+== Installation
First you need to download the Rodin platform (e.g,
http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.3/[Rodin
@@ -30,7 +31,7 @@ A detailed
of the installation is available here>>.
[[starting-prob-tutorial-rodin-first-step]]
-==== Starting ProB
+== Starting ProB
Start by right clicking (control Click on the Mac) on the machine or
context you wish to animate and select "Start Animation/Model
diff --git a/src/docs/chapter/user/30_OtherLanguages/EventB/Tutorial_Rodin_Parameters.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Rodin_Parameters.adoc
similarity index 94%
rename from src/docs/chapter/user/30_OtherLanguages/EventB/Tutorial_Rodin_Parameters.adoc
rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Rodin_Parameters.adoc
index 7f06380..367b6a8 100644
--- a/src/docs/chapter/user/30_OtherLanguages/EventB/Tutorial_Rodin_Parameters.adoc
+++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Rodin_Parameters.adoc
@@ -1,8 +1,9 @@
+
[[tutorial-rodin-parameters]]
-=== Tutorial Rodin Parameters
+= Tutorial Rodin Parameters
[[preferences-tutorial-rodin-parameters]]
-==== Preferences
+== Preferences
You can modify the most important parameters of ProB by going to the
Rodin preferences.
@@ -18,7 +19,7 @@ image::ProBRodinPrefs.png[]
We explain the most important preferences below.
[[minint-and-maxint]]
-==== Minint and Maxint
+== Minint and Maxint
We first explain the first two entries in the screenshot above. Within
classical B this provides the range for the implementable integer type.
@@ -28,7 +29,7 @@ if it cannot determine the value of an integer variable in order to know
in which range it should be enumerated.
[[size-of-unspecified-sets-carrier-sets]]
-==== Size of unspecified sets (carrier sets)
+== Size of unspecified sets (carrier sets)
This is the third entry in the screen shot above. ProB requires all
carrier sets to be finite and ProB has to know the cardinality before
@@ -44,7 +45,7 @@ specify a maximum cardinality, or `card(S)>n` to specify a minimum
cardinality.
[[using-contexts-for-prob-animation]]
-===== Using contexts for ProB animation
+=== Using contexts for ProB animation
Note that you can create a new context with those axioms just for
animation or model checking with ProB. For this you can simply
diff --git a/src/docs/chapter/user/10_General/Tutorial_Setup_Phases.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Setup_Phases.adoc
similarity index 98%
rename from src/docs/chapter/user/10_General/Tutorial_Setup_Phases.adoc
rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Setup_Phases.adoc
index 266d92b..f14b8d9 100644
--- a/src/docs/chapter/user/10_General/Tutorial_Setup_Phases.adoc
+++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Setup_Phases.adoc
@@ -1,5 +1,6 @@
+
[[tutorial-setup-phases]]
-== Tutorial Setup Phases
+= Tutorial Setup Phases
We assume that you have grasped the first steps of opening and animating
a B machine as outlined in <<tutorial-first-step,Tutorial First
@@ -30,7 +31,7 @@ image::ProB_AnimationPhases.png[]
We now examine these phases on the Jukebox machine in more detail
[[loading]]
-=== 1. Loading
+== 1. Loading
Here ProB parses and type checks the machine.
@@ -71,7 +72,7 @@ a "Reopen" command in the _File_ menu:
image::ProB_JukeboxReopenCommand.png[]
[[setup_constants]]
-=== 2. SETUP_CONSTANTS
+== 2. SETUP_CONSTANTS
In this phase ProB will try and find values for the constants and
parameters of your machine, so that the `PROPERTIES` and `CONSTRAINTS`
@@ -90,7 +91,7 @@ phase:
image::ProB_JukeboxAfterSETUPCONSTANTS.png[]
[[initialisation]]
-=== 3. INITIALISATION
+== 3. INITIALISATION
In this phase the values for the constants have been found, but the
initial values of the variables still remain to be determined. For this,
diff --git a/src/docs/chapter/user/40_AdvancedFeatures/10_Tutorials/Tutorial_Symbolic_Constants.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Symbolic_Constants.adoc
similarity index 91%
rename from src/docs/chapter/user/40_AdvancedFeatures/10_Tutorials/Tutorial_Symbolic_Constants.adoc
rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Symbolic_Constants.adoc
index 395c72b..7762b69 100644
--- a/src/docs/chapter/user/40_AdvancedFeatures/10_Tutorials/Tutorial_Symbolic_Constants.adoc
+++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Symbolic_Constants.adoc
@@ -1,8 +1,9 @@
+
[[tutorial-symbolic-constants]]
-== Tutorial Symbolic Constants
+= Tutorial Symbolic Constants
[[introduction-to-tutorial-symbolic-constants]]
-=== Introduction
+== Introduction
ProB Tcl/Tk as well as the
<<using-the-command-line-version-of-prob,probcli command-line
@@ -14,14 +15,14 @@ complex ones.
Through a plugin, this behaviour is extended to ProB for Rodin.
[[installing-the-prob-symbolic-constants-plugin]]
-=== Installing the ProB Symbolic Constants Plugin
+== Installing the ProB Symbolic Constants Plugin
The plugin is available from the ProB for Rodin Updatesite. The package
is called "ProB for Rodin2 - Symbolic Constants Support". It is not
bundled with ProB for Rodin itself.
[[marking-constants-to-be-kept-symbolic]]
-=== Marking Constants to be kept symbolic
+== Marking Constants to be kept symbolic
Once the plugin is installed, a toggle button "symbolic" / "not
symbolic" should appear next to each constant in the Rodin editor.
diff --git a/src/docs/chapter/user/10_General/Tutorial_Troubleshooting_the_Setup.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Troubleshooting_the_Setup.adoc
similarity index 98%
rename from src/docs/chapter/user/10_General/Tutorial_Troubleshooting_the_Setup.adoc
rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Troubleshooting_the_Setup.adoc
index e77e4fa..9bc968f 100644
--- a/src/docs/chapter/user/10_General/Tutorial_Troubleshooting_the_Setup.adoc
+++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Troubleshooting_the_Setup.adoc
@@ -1,5 +1,6 @@
+
[[tutorial-troubleshooting-the-setup]]
-== Tutorial Troubleshooting the Setup
+= Tutorial Troubleshooting the Setup
We assume that you have grasped the way that ProB setups up the initial
states of a B machine as outlined in
@@ -15,7 +16,7 @@ We will also learn to use the various predicate analysis features
provided by ProB.
[[simple-inconsistency-in-the-properties]]
-=== Simple Inconsistency in the PROPERTIES
+== Simple Inconsistency in the PROPERTIES
First, open the machine "Jukebox.mch" which can be found in the
SchneiderBook/Jukebox_Chapter13 subdirectory of the ProB Examples
@@ -70,7 +71,7 @@ we can proceed with animation of the machine:
image::ProB_JukeboxAfterLoad2.png[]
[[a-more-involved-inconsistency]]
-=== A more involved inconsistency
+== A more involved inconsistency
Let us add
diff --git a/src/docs/chapter/user/10_General/Tutorial_Understanding_ProB's_Constraint_Solver.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Understanding_ProB's_Constraint_Solver.adoc
similarity index 98%
rename from src/docs/chapter/user/10_General/Tutorial_Understanding_ProB's_Constraint_Solver.adoc
rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Understanding_ProB's_Constraint_Solver.adoc
index 9a16801..b5e4ac7 100644
--- a/src/docs/chapter/user/10_General/Tutorial_Understanding_ProB's_Constraint_Solver.adoc
+++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Understanding_ProB's_Constraint_Solver.adoc
@@ -1,5 +1,6 @@
+
[[tutorial-understanding-probs-constraint-solver]]
-== Tutorial Understanding ProB's Constraint Solver
+= Tutorial Understanding ProB's Constraint Solver
We assume that you have grasped the way that ProB setups up the initial
states of a B machine as outlined in
@@ -71,7 +72,7 @@ The following picture provides a very rough picture of this process:
image::ProB_Propagation.png[]
-=== A simple example
+== A simple example
Let us use the following B machine as starting point:
@@ -161,7 +162,7 @@ and fi are correct (by looking at the "State Properties" pane):
image::ProB_PropagationAfterInit.png[]
[[complicating-the-example]]
-=== Complicating the Example
+== Complicating the Example
To make the example more challenging, let us increase `up` to 100 and
remove the equality for `f`. In other words, the PROPERTIES will now
@@ -246,7 +247,7 @@ ms)"" in the "Animation Preferences". You can also control it using a
definition for `SET_PREF_TIME_OUT` in the DEFINITIONS clause.
[[adding-universally-quantified-formulas]]
-=== Adding universally quantified formulas
+== Adding universally quantified formulas
Let us replace `f=fi` by the following property:
diff --git a/src/docs/chapter/user/10_General/Tutorial_Understanding_the_Complexity_of_B_Animation.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Understanding_the_Complexity_of_B_Animation.adoc
similarity index 98%
rename from src/docs/chapter/user/10_General/Tutorial_Understanding_the_Complexity_of_B_Animation.adoc
rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Understanding_the_Complexity_of_B_Animation.adoc
index 0352f01..fb4efe7 100644
--- a/src/docs/chapter/user/10_General/Tutorial_Understanding_the_Complexity_of_B_Animation.adoc
+++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Understanding_the_Complexity_of_B_Animation.adoc
@@ -1,5 +1,6 @@
+
[[tutorial-understanding-the-complexity-of-b-animation]]
-== Tutorial Understanding the Complexity of B Animation
+= Tutorial Understanding the Complexity of B Animation
We assume that you have grasped the way that ProB setups up the initial
states of a B machine as outlined in
@@ -10,7 +11,7 @@ general, how ProB solves this problem, and what the ramification for
users are.
[[undecidability]]
-=== Undecidability
+== Undecidability
In general, animation of a B model is undecidable. More precisely, it is
undecidable to find out
@@ -72,7 +73,7 @@ deferred set to a finite number before animation (see also
you can control the cardinality of the deferred sets).
[[complexity-of-animation]]
-=== Complexity of Animation
+== Complexity of Animation
However, after addressing the undecidability issue, there is still the
problem of complexity. The animation task can be arbitrarily complex
diff --git a/src/docs/chapter/user/40_AdvancedFeatures/10_Tutorials/Tutorial_Unit_Plugin.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Unit_Plugin.adoc
similarity index 95%
rename from src/docs/chapter/user/40_AdvancedFeatures/10_Tutorials/Tutorial_Unit_Plugin.adoc
rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Unit_Plugin.adoc
index 40d3e0b..6f416f6 100644
--- a/src/docs/chapter/user/40_AdvancedFeatures/10_Tutorials/Tutorial_Unit_Plugin.adoc
+++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Unit_Plugin.adoc
@@ -1,5 +1,6 @@
+
[[tutorial-unit-plugin]]
-== Tutorial Unit Plugin
+= Tutorial Unit Plugin
This tutorial describes, how ProB's integrated plugin for unit analysis
can be used to verify the usage of physical units throughout a B
@@ -17,7 +18,7 @@ We assume that you have a general understanding of B and the usage of
ProB.
[[activating-the-plugin-and-setting-preferences]]
-=== Activating the Plugin and setting preferences
+== Activating the Plugin and setting preferences
Currently, the plugin can only be used with classical B machines.
Therefore, a B machine needs to be loaded before the plugin can be
@@ -41,7 +42,7 @@ a fix point state, in which possible unit errors are presented to the
user through ProB's error reporting facilities.
[[annotating-variables-and-animating-a-machine]]
-=== Annotating variables and animating a machine
+== Annotating variables and animating a machine
To connect a variable with an expected physical unit, a special comment
is placed before the variable.
@@ -73,7 +74,7 @@ enables the plugin to be used in conjunction with the evaluation view,
the dot output and most other ProB features.
[[converting-between-units]]
-=== Converting between units
+== Converting between units
To distinct between a numerical multiplication, that changes the values
without changing the unit and a multiplication meant to convert between
@@ -101,7 +102,7 @@ END
....
[[static-analysis]]
-=== Static analysis
+== Static analysis
If activated, the results of the static analysis can be accessed from
the plugin menu. Currently, the results include the inferred unit of
diff --git a/src/docs/chapter/user/40_AdvancedFeatures/10_Tutorials/Tutorial_Unit_Plugin_With_Rodin.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Unit_Plugin_With_Rodin.adoc
similarity index 92%
rename from src/docs/chapter/user/40_AdvancedFeatures/10_Tutorials/Tutorial_Unit_Plugin_With_Rodin.adoc
rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Unit_Plugin_With_Rodin.adoc
index 8fb62ae..14e1c5e 100644
--- a/src/docs/chapter/user/40_AdvancedFeatures/10_Tutorials/Tutorial_Unit_Plugin_With_Rodin.adoc
+++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Unit_Plugin_With_Rodin.adoc
@@ -1,5 +1,6 @@
+
[[tutorial-unit-plugin-with-rodin]]
-== Tutorial Unit Plugin With Rodin
+= Tutorial Unit Plugin With Rodin
This tutorial describes, how ProB's integrated plugin for unit analysis
can be used with Event-B machines from inside the Rodin platform. This
@@ -18,7 +19,7 @@ We assume that you have a general understanding of Event-B and the usage
of ProB / Rodin.
[[installing-physical-units-support-for-prob-for-rodin]]
-=== Installing Physical Units Support for ProB for Rodin
+== Installing Physical Units Support for ProB for Rodin
You can follow the <<tutorial-rodin-first-step,First Steps
Instructions>> or the
@@ -30,7 +31,7 @@ Rodin2 - Physical Units Support" plugin at out Rodin update site. You
have to install both to enable physical units support for Rodin.
[[attaching-physical-units-to-variables-and-constants]]
-=== Attaching Physical Units to Variables and Constants
+== Attaching Physical Units to Variables and Constants
Once both plugins are installed, ProB allows to annotate both variables
and constants with physical units:
@@ -47,7 +48,7 @@ Units can be supplied in two forms:
"10^2 * m^2".
[[starting-the-analysis]]
-=== Starting the Analysis
+== Starting the Analysis
The supplied units can now be used by ProB to infer missing units,
verify the supplied units and detect unit errors. To start the analysis
@@ -60,7 +61,7 @@ Once the analysis is finished, the "inferred unit" text fields are
filled with the resulting units.
[[possible-errors]]
-=== Possible Errors
+== Possible Errors
Inside the Rodin Errors view, several errors might occur:
diff --git a/src/docs/chapter/user/20_Validation/MC/Tutorial_Various_Optimizations.adoc b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Various_Optimizations.adoc
similarity index 99%
rename from src/docs/chapter/user/20_Validation/MC/Tutorial_Various_Optimizations.adoc
rename to src/docs/chapter/user/YZ_Tutorials/Tutorial_Various_Optimizations.adoc
index a833386..2a20d48 100644
--- a/src/docs/chapter/user/20_Validation/MC/Tutorial_Various_Optimizations.adoc
+++ b/src/docs/chapter/user/YZ_Tutorials/Tutorial_Various_Optimizations.adoc
@@ -1,5 +1,6 @@
+
[[tutorial-various-optimizations]]
-== Tutorial Various Optimizations
+= Tutorial Various Optimizations
The ordinary model checker of ProB enables the user to verify
automatically whether a B model contains any errors such as deadlocks
@@ -20,7 +21,7 @@ additionally gives hints when it is recommendable to use these
optimizations.
[[partial-order-reduction]]
-=== Partial Order Reduction
+== Partial Order Reduction
Partial order reduction (POR) is a method proposed for combating the
state space explosion problem by means of state space reduction. The
@@ -220,7 +221,7 @@ models. The evaluation can be obtained
https://www3.hhu.de/stups/downloads/[here].
[[partial-guard-evaluation]]
-=== Partial Guard Evaluation
+== Partial Guard Evaluation
When checking for consistency a B model the ProB model checker traverses
the state space of the model beginning in some of the initial states and
@@ -534,4 +535,4 @@ These and various other benchmarks used for evaluating partial guard
evaluation (PGE) can be viewed
https://www3.hhu.de/stups/downloads/[here].
-=== References
+== References
diff --git a/src/docs/chapter/user/YZ_Tutorials/ZZ_section_footer.adoc b/src/docs/chapter/user/YZ_Tutorials/ZZ_section_footer.adoc
new file mode 100644
index 0000000..47b3e87
--- /dev/null
+++ b/src/docs/chapter/user/YZ_Tutorials/ZZ_section_footer.adoc
@@ -0,0 +1,3 @@
+
+
+:leveloffset: -1
diff --git a/src/docs/chapter/user/70_Appendix/00_Appendix.adoc b/src/docs/chapter/user/ZZ_Appendix/00_section_header.adoc
similarity index 57%
rename from src/docs/chapter/user/70_Appendix/00_Appendix.adoc
rename to src/docs/chapter/user/ZZ_Appendix/00_section_header.adoc
index 2f15ee7..b5aa2d0 100644
--- a/src/docs/chapter/user/70_Appendix/00_Appendix.adoc
+++ b/src/docs/chapter/user/ZZ_Appendix/00_section_header.adoc
@@ -1,2 +1,4 @@
+
[[appendix]]
= Appendix
+:leveloffset: +1
diff --git a/src/docs/chapter/user/70_Appendix/01_Team.adoc b/src/docs/chapter/user/ZZ_Appendix/01_Team.adoc
similarity index 99%
rename from src/docs/chapter/user/70_Appendix/01_Team.adoc
rename to src/docs/chapter/user/ZZ_Appendix/01_Team.adoc
index 17e2ef7..a598bb8 100644
--- a/src/docs/chapter/user/70_Appendix/01_Team.adoc
+++ b/src/docs/chapter/user/ZZ_Appendix/01_Team.adoc
@@ -1,5 +1,5 @@
[[team]]
-== Team
+= Team
ProB is based on research and implemention effort by our https://www.cs.hhu.de/lehrstuehle-und-arbeitsgruppen/softwaretechnik-und-programmiersprachen/unser-team.html[team]:
* Michael Leuschel,
diff --git a/src/docs/chapter/user/70_Appendix/02_FAQ.adoc b/src/docs/chapter/user/ZZ_Appendix/02_FAQ.adoc
similarity index 91%
rename from src/docs/chapter/user/70_Appendix/02_FAQ.adoc
rename to src/docs/chapter/user/ZZ_Appendix/02_FAQ.adoc
index a66f8ea..a2ba12f 100644
--- a/src/docs/chapter/user/70_Appendix/02_FAQ.adoc
+++ b/src/docs/chapter/user/ZZ_Appendix/02_FAQ.adoc
@@ -1,13 +1,13 @@
[[faq]]
-== FAQ : Frequently asked Questions
+= FAQ : Frequently asked Questions
-=== Can I use transitive closure for Event-B models?
+== Can I use transitive closure for Event-B models?
Yes, you need to use a theory of the transitive closure which contains a
special mapping file. See <<event-b-theories,the section about Event-B theories>> along with the links to theories that can be used
efficiently with ProB.
-=== How can I reduce the memory consumption for model-checking?
+== How can I reduce the memory consumption for model-checking?
There are several options:
@@ -32,7 +32,7 @@ checking, especially when the branching factor is very high.
will not work for refinements and only has limited support for machine
inclusion, but it can be very fast and the state space is kept on disk.
-=== How do I perform a self-check of ProB?
+== How do I perform a self-check of ProB?
If you suspect something is wrong with your ProB Tcl/Tk installation,
run the "Perform Self Check" command in the "Debug Menu". Note: run
@@ -53,7 +53,7 @@ Self-Check Finished
-------------------
....
-=== ProB seems stuck when loading a machine
+== ProB seems stuck when loading a machine
After parsing a machine, ProB is attempting to find valid initial states
of your machine (or in case your machine has constants, valid values of
@@ -67,7 +67,7 @@ jbtools parser sometimes behaves badly when syntax errors are present
and can take a very long time to return the syntax error. [This has been
fixed in the release 1.2.0]
-=== Which features of B are covered?
+== Which features of B are covered?
ProB covers a large part of B, and we are striving towards full
coverage. ProB supports B features such as non-deterministic operations,
@@ -77,7 +77,7 @@ properties, and many more. It has limited support for multiple machines
and refinements (see the <<Current_Limitations.adoc, Current_Limitations>>
section and the FAQ entry about refinements below).
-=== Is there support for refinement?
+== Is there support for refinement?
For the moment, you have to give types to operation arguments in
refinements; the types are not always extracted from the ancestor
@@ -96,7 +96,7 @@ affects refinement checking. [ProB's refinement checker is more suited
for EventB than classical B, but we are working to fully support both
styles of refinement.]
-=== The constraint based checker is very slow and does not always work
+== The constraint based checker is very slow and does not always work
The constraint based checker is the least stable part of the system.
@@ -109,12 +109,12 @@ the constraint based checker, not in the temporal model checker or the
animator). Running ProB on Sicstus Prolog 3.9 seems to get rid of this
problem (at least partially).
-=== I can animate your machine files but I am not able to open my own machine files
+== I can animate your machine files but I am not able to open my own machine files
Be sure to have Java installed and set up the CLASSPATH as stipulated
above.
-=== ProB complains that some variables are not given a proper type
+== ProB complains that some variables are not given a proper type
All variables should be given a type even though ProB may still work
without them (but you are living dangerously). In the latest release,
@@ -124,14 +124,14 @@ also recognized as a type. aa: POW(myset) & bb: POW(aa) is now ok
POW(POW(myset)) ). One can now also use subset for typing: bb <:
COLOURS.
-=== I cannot visualize the state space
+== I cannot visualize the state space
Be sure to set up the viewer preferences and use / (even on Windows!) Be
sure to have dot installed and either dotty or a Postscript viewer.
Also, on Windows the path to the machine files should not contain
spaces. A good example directory would be C:/Machines/
-=== Some of my machines do not behave as expected
+== Some of my machines do not behave as expected
Maybe you are using a feature of B not yet supported by ProB. Have a
look at the console window and see whether ProB displays any warning
@@ -142,7 +142,7 @@ Machine and a description of the problem to me. You can also use the
Save State Command in the File Menu and then send me the *.saved.P file
(this way you do not have to tell me how to reach the buggy state).
-=== How does ProB treat INT and NAT as opposed to INTEGER and NATURAL?
+== How does ProB treat INT and NAT as opposed to INTEGER and NATURAL?
As of version 1.2 ProB treats INT differently from INTEGER (the same is
true for NAT and NAT1). A variable x:INT is now required to lie between
@@ -150,7 +150,7 @@ MININT..MAXINT (which can be changed in the preferences; you can also
change the setting on a per machine basis by adding DEFINITIONS
likeSET_PREF_MININT == -10; SET_PREF_MAXINT == 100; to your machine.)
-=== Problem with libtk.so on Linux
+== Problem with libtk.so on Linux
When launching ProB on Linux I get: ./prob: error while loading shared
libraries: /usr/lib/libtk.so : invalid ELF header
@@ -164,7 +164,7 @@ e.g., do something like that: # ln -s /usr/lib/libtk8.4.s
(Probably best to make a backup of libtk.so before that.)
----
-=== Finding Multiple Assertion Violations
+== Finding Multiple Assertion Violations
I want to generate multiple assertion violations in ProB in order to
generate the customized test cases for a particular B specfication
@@ -182,7 +182,7 @@ my_assertion_N = SELECT not(Assertion_N) THEN skip END After model
checking, you can again use "Compute Coverage" to see how often every
assertion has been violated.
-=== Checking Multiple LTL Formulas
+== Checking Multiple LTL Formulas
Can multiple LTL formulas be verified at a time?
diff --git a/src/docs/chapter/user/70_Appendix/03_Download.adoc b/src/docs/chapter/user/ZZ_Appendix/03_Download.adoc
similarity index 91%
rename from src/docs/chapter/user/70_Appendix/03_Download.adoc
rename to src/docs/chapter/user/ZZ_Appendix/03_Download.adoc
index 1d689d3..3156f75 100644
--- a/src/docs/chapter/user/70_Appendix/03_Download.adoc
+++ b/src/docs/chapter/user/ZZ_Appendix/03_Download.adoc
@@ -1,4 +1,4 @@
[[downloads]]
-== Download
+= Download
If you click https://www3.hhu.de/stups/prob/index.php/Download[here] you will be redirected to our online Download page.
diff --git a/src/docs/chapter/user/70_Appendix/04_DownloadPriorVersions.adoc b/src/docs/chapter/user/ZZ_Appendix/04_DownloadPriorVersions.adoc
similarity index 87%
rename from src/docs/chapter/user/70_Appendix/04_DownloadPriorVersions.adoc
rename to src/docs/chapter/user/ZZ_Appendix/04_DownloadPriorVersions.adoc
index 80dc5f5..24041c6 100644
--- a/src/docs/chapter/user/70_Appendix/04_DownloadPriorVersions.adoc
+++ b/src/docs/chapter/user/ZZ_Appendix/04_DownloadPriorVersions.adoc
@@ -1,4 +1,4 @@
[[prior-versions-of-prob]]
-== Prior Versions of ProB
+= Prior Versions of ProB
If you click https://www3.hhu.de/stups/prob/index.php/DownloadPriorVersions[here] you will be redirected to the Download Prior Versions of ProB page.
diff --git a/src/docs/chapter/user/70_Appendix/05_Links.adoc b/src/docs/chapter/user/ZZ_Appendix/05_Links.adoc
similarity index 98%
rename from src/docs/chapter/user/70_Appendix/05_Links.adoc
rename to src/docs/chapter/user/ZZ_Appendix/05_Links.adoc
index 51a11c0..c5ba633 100644
--- a/src/docs/chapter/user/70_Appendix/05_Links.adoc
+++ b/src/docs/chapter/user/ZZ_Appendix/05_Links.adoc
@@ -1,8 +1,8 @@
[[links]]
-== Links
+= Links
[[books]]
-=== Books
+== Books
* http://www.jpbowen.com/publications/thes-b.html[The B-Book: Assigning
programs to meanings, by Jean-Raymond Abrial] (link is to a review by
@@ -13,7 +13,7 @@ Introduction, by Steve Schneider]
Software Engineering, by Jean-Raymond Abrial] (the Bee book)
[[papers]]
-=== Papers
+== Papers
* https://www3.hhu.de/stups/downloads/pdf/[ProB Publications]
* http://en.wikipedia.org/wiki/B-Method[B-Method in Wikipedia]
@@ -23,7 +23,7 @@ FM tools manage large scale industrial problems ?]
* http://www.data-validation.fr[Data Validation]
[[prob]]
-=== ProB
+== ProB
* <<modelling-examples,Examples for ProB>> (along with screenshots and
explanations)
@@ -34,7 +34,7 @@ to Success Story (written by Cetic)]
* https://groups.google.com/d/forum/prob-users[prob-users group]
[[tools-using-prob]]
-=== Tools using ProB
+== Tools using ProB
* https://github.com/plues/plues[PLUES] tool for university course
validation
@@ -79,7 +79,7 @@ implicit VDM specifications inside Ouverture]
* http://www.ovado.net[Ovado] (as second tool chain)
[[related-tools]]
-=== Related Tools
+== Related Tools
* http://www.atelierb.eu/[Atelier B]
* http://www.event-b.org/[Event-B and Rodin Wiki]
@@ -105,7 +105,7 @@ TLA+, CSP and Prolog]
checking tools]
[[testimonials]]
-=== Testimonials
+== Testimonials
* http://www.deploy-project.eu/pdf/D41-Siemens-final-full.pdf[Data
validation at Siemens, Jérôme Falampin]: "The work done with ProB is a
@@ -188,12 +188,12 @@ competition] (this is ProB out-of-the-box, without tuning and where SMT
formulas are translated to B)
[[other-links]]
-=== Other Links
+== Other Links
* https://github.com/klar42/railground/[Railground Event-B Model]
[[translating-to-logic]]
-=== Translating to Logic
+== Translating to Logic
* http://legacy.earlham.edu/~peters/courses/log/transtip.htm[Translation
Tips]
diff --git a/src/docs/chapter/user/70_Appendix/06_ProB_Release_History.adoc b/src/docs/chapter/user/ZZ_Appendix/06_ProB_Release_History.adoc
similarity index 99%
rename from src/docs/chapter/user/70_Appendix/06_ProB_Release_History.adoc
rename to src/docs/chapter/user/ZZ_Appendix/06_ProB_Release_History.adoc
index 60e9268..5c86345 100644
--- a/src/docs/chapter/user/70_Appendix/06_ProB_Release_History.adoc
+++ b/src/docs/chapter/user/ZZ_Appendix/06_ProB_Release_History.adoc
@@ -1,5 +1,5 @@
[[release-history]]
-== ProB Release History
+= ProB Release History
Full ProB release history until release 1.8.3:
diff --git a/src/docs/chapter/user/70_Appendix/10_Bugs.adoc b/src/docs/chapter/user/ZZ_Appendix/10_Bugs.adoc
similarity index 97%
rename from src/docs/chapter/user/70_Appendix/10_Bugs.adoc
rename to src/docs/chapter/user/ZZ_Appendix/10_Bugs.adoc
index 70df84d..6b43847 100644
--- a/src/docs/chapter/user/70_Appendix/10_Bugs.adoc
+++ b/src/docs/chapter/user/ZZ_Appendix/10_Bugs.adoc
@@ -1,5 +1,5 @@
[[bugs]]
-== Bugs
+= Bugs
If you want to submit a bug report, please use our https://probjira.atlassian.net/projects/PROBCORE/issues/[bug tracker]. You may
also want to ask questions within our https://groups.google.com/forum/#!forum/prob-users[prob-users group].
diff --git a/src/docs/chapter/user/70_Appendix/11_Troubleshooting.adoc b/src/docs/chapter/user/ZZ_Appendix/11_Troubleshooting.adoc
similarity index 98%
rename from src/docs/chapter/user/70_Appendix/11_Troubleshooting.adoc
rename to src/docs/chapter/user/ZZ_Appendix/11_Troubleshooting.adoc
index 12cce01..6882188 100644
--- a/src/docs/chapter/user/70_Appendix/11_Troubleshooting.adoc
+++ b/src/docs/chapter/user/ZZ_Appendix/11_Troubleshooting.adoc
@@ -1,5 +1,5 @@
[[troubleshooting]]
-== Troubleshooting
+= Troubleshooting
* Avoid installing ProB in a path with spaces or other special
characters in them. The same holds for B machines you wish to analyze
diff --git a/src/docs/chapter/user/70_Appendix/20_ProBLicence.adoc b/src/docs/chapter/user/ZZ_Appendix/20_ProBLicence.adoc
similarity index 98%
rename from src/docs/chapter/user/70_Appendix/20_ProBLicence.adoc
rename to src/docs/chapter/user/ZZ_Appendix/20_ProBLicence.adoc
index a4bc7d2..159f856 100644
--- a/src/docs/chapter/user/70_Appendix/20_ProBLicence.adoc
+++ b/src/docs/chapter/user/ZZ_Appendix/20_ProBLicence.adoc
@@ -1,5 +1,5 @@
[[prob-licence]]
-== ProB Licence
+= ProB Licence
The ProB source code is distributed under the
http://www.eclipse.org/org/documents/epl-v10.html[EPL v1.0 license] (see
diff --git a/src/docs/chapter/appendix/A_literature.adoc b/src/docs/chapter/user/ZZ_Appendix/A_literature.adoc
similarity index 97%
rename from src/docs/chapter/appendix/A_literature.adoc
rename to src/docs/chapter/user/ZZ_Appendix/A_literature.adoc
index 1092fb5..a73a734 100644
--- a/src/docs/chapter/appendix/A_literature.adoc
+++ b/src/docs/chapter/user/ZZ_Appendix/A_literature.adoc
@@ -1,3 +1,4 @@
+
= Additional Literature
bibliography::[]
diff --git a/src/docs/chapter/appendix/B_preferences.adoc b/src/docs/chapter/user/ZZ_Appendix/B_preferences.adoc
similarity index 99%
rename from src/docs/chapter/appendix/B_preferences.adoc
rename to src/docs/chapter/user/ZZ_Appendix/B_preferences.adoc
index 7dab0dc..3a28b02 100644
--- a/src/docs/chapter/appendix/B_preferences.adoc
+++ b/src/docs/chapter/user/ZZ_Appendix/B_preferences.adoc
@@ -1,3 +1,4 @@
+
= ProB Preferences
A list of the current preferences available in ProB is available <<preferences-for-command-line,here>>.
diff --git a/src/docs/chapter/user/ZZ_Appendix/ZZ_section_footer.adoc b/src/docs/chapter/user/ZZ_Appendix/ZZ_section_footer.adoc
new file mode 100644
index 0000000..47b3e87
--- /dev/null
+++ b/src/docs/chapter/user/ZZ_Appendix/ZZ_section_footer.adoc
@@ -0,0 +1,3 @@
+
+
+:leveloffset: -1
--
GitLab