Commit b9781777 authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[cmd] Add doc for start, invariant, final properties

parent e46e727f
...@@ -292,7 +292,8 @@ def main(): ...@@ -292,7 +292,8 @@ def main():
parser_input_file.add_argument('chart_file') parser_input_file.add_argument('chart_file')
# Get final_property alone OR an input_file containing multiple properties # Get final_property alone OR an input_file containing multiple properties
group = parser_input_file.add_mutually_exclusive_group(required=True) 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='?', group.add_argument('--input_file', action=ReadableFile, nargs='?',
help="Without input file, there will be only one process. " help="Without input file, there will be only one process. "
"While there will be 1 process per line (per logical formula " "While there will be 1 process per line (per logical formula "
...@@ -317,8 +318,14 @@ def main(): ...@@ -317,8 +318,14 @@ def main():
parser_input_file.add_argument('--continue', action='store_true', parser_input_file.add_argument('--continue', action='store_true',
help="Resume previous computations; if there is a mac file from a " help="Resume previous computations; if there is a mac file from a "
"previous work, last frontier places/boundaries will be reloaded.") "previous work, last frontier places/boundaries will be reloaded.")
parser_input_file.add_argument('--start_prop', nargs='?', default=None) parser_input_file.add_argument('--start_prop', nargs='?', default=None,
parser_input_file.add_argument('--inv_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) parser_input_file.set_defaults(func=solutions_search)
......
...@@ -23,6 +23,9 @@ ...@@ -23,6 +23,9 @@
# 35042 RENNES Cedex, FRANCE # 35042 RENNES Cedex, FRANCE
""" """
Search Minimal Accessibility Conditions 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 unicode_literals
from __future__ import print_function from __future__ import print_function
...@@ -138,8 +141,14 @@ def main2(chart_file, mac_file, mac_step_file, mac_complete_file, mac_strong_fil ...@@ -138,8 +141,14 @@ def main2(chart_file, mac_file, mac_step_file, mac_complete_file, mac_strong_fil
:param mac_strong_file: ??? :param mac_strong_file: ???
:param steps: Maximal steps to reach the solutions. :param steps: Maximal steps to reach the solutions.
:param final_prop: Formula: Property that the solver looks for. :param final_prop: Formula: Property that the solver looks for.
:param start_prop: Formula: Original property (constraint) for the solver. ## TODO :param start_prop: Formula: Property that will be part of the initial state
:param inv_prop: Formula: ???## TODO 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 :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`. 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 If set to False: The solver will search all solutions with the minimum
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment