From b97817776e71366025431655ab20bff1ba849f77 Mon Sep 17 00:00:00 2001
From: VIGNET Pierre <pierre.vignet@irisa.fr>
Date: Thu, 21 Nov 2019 17:46:24 +0100
Subject: [PATCH] [cmd] Add doc for start, invariant, final properties
---
command_line/cadbiom_cmd/cadbiom_cmd.py | 13 ++++++++++---
command_line/cadbiom_cmd/solution_search.py | 13 +++++++++++--
2 files changed, 21 insertions(+), 5 deletions(-)
diff --git a/command_line/cadbiom_cmd/cadbiom_cmd.py b/command_line/cadbiom_cmd/cadbiom_cmd.py
index cb2a659..567d9b6 100644
--- a/command_line/cadbiom_cmd/cadbiom_cmd.py
+++ b/command_line/cadbiom_cmd/cadbiom_cmd.py
@@ -292,7 +292,8 @@ def main():
parser_input_file.add_argument('chart_file')
# Get final_property alone OR an input_file containing multiple properties
group = parser_input_file.add_mutually_exclusive_group(required=True)
- group.add_argument('final_prop', nargs='?')
+ group.add_argument('final_prop', nargs='?',
+ help="Final property that will occur at the end of the simulation.")
group.add_argument('--input_file', action=ReadableFile, nargs='?',
help="Without input file, there will be only one process. "
"While there will be 1 process per line (per logical formula "
@@ -317,8 +318,14 @@ def main():
parser_input_file.add_argument('--continue', action='store_true',
help="Resume previous computations; if there is a mac file from a "
"previous work, last frontier places/boundaries will be reloaded.")
- parser_input_file.add_argument('--start_prop', nargs='?', default=None)
- parser_input_file.add_argument('--inv_prop', nargs='?', default=None)
+ parser_input_file.add_argument('--start_prop', nargs='?', default=None,
+ help="Property that will be part of the initial state of the model. "
+ "In concrete terms, some entities can be activated by this "
+ "mechanism without modifying the model.")
+ parser_input_file.add_argument('--inv_prop', nargs='?', default=None,
+ help="Invariant property that will never occur during the simulation. "
+ "The given logical formula will be enclose by a logical not() and "
+ "will be checked at each step of the simulation.")
parser_input_file.set_defaults(func=solutions_search)
diff --git a/command_line/cadbiom_cmd/solution_search.py b/command_line/cadbiom_cmd/solution_search.py
index 2490b9f..8a44852 100644
--- a/command_line/cadbiom_cmd/solution_search.py
+++ b/command_line/cadbiom_cmd/solution_search.py
@@ -23,6 +23,9 @@
# 35042 RENNES Cedex, FRANCE
"""
Search Minimal Accessibility Conditions
+
+Simulation of the system until some halting condition (given with the final
+property) is satisfied.
"""
from __future__ import unicode_literals
from __future__ import print_function
@@ -138,8 +141,14 @@ def main2(chart_file, mac_file, mac_step_file, mac_complete_file, mac_strong_fil
:param mac_strong_file: ???
:param steps: Maximal steps to reach the solutions.
:param final_prop: Formula: Property that the solver looks for.
- :param start_prop: Formula: Original property (constraint) for the solver. ## TODO
- :param inv_prop: Formula: ???## TODO
+ :param start_prop: Formula: Property that will be part of the initial state
+ of the model.
+ In concrete terms, some entities can be activated by this mechanism
+ without modifying the model.
+ :param inv_prop: Formula: Invariant property that will never occur during
+ the simulation.
+ The given logical formula will be enclose by a logical not() and
+ will be checked at each step of the simulation.
:param all_macs: If set to True (not default), search all macs with
less or equal the maxium of steps defined with the argument `steps`.
If set to False: The solver will search all solutions with the minimum
--
GitLab