Commit 59b932a0 authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

Add some doc on bloatware...

parent 00fcb322
......@@ -142,7 +142,20 @@ class CLUnfolder(object):
# constraints - logical constraints
# result from unfolding of base constraints
# Boolean vectors signification:
# X: Current state of places (activated/unactivated)
# X': Future state of places
# H: Current 'free' events (present/not present) => ?
# I: Current inputs => ?
self.__dynamic_constraints = [] # DIMACS clauses: X' = f(X,H,I)
# Simple temporal properties
# SP(X0): Initial property/start property; Never change at each step.
# IP(X): Invariant property
# VP(X): Variant property;
# List of logical formulas of properties forced at each step
# FP(X): Final property
self.__initial_constraints = [] # DIMACS clauses: C(X_0)
self.__final_constraints = [] # idem: C(X_n)
self.__invariant_constraints = [] # DIMACS clauses: C(X_i))
......@@ -706,8 +719,10 @@ class CLUnfolder(object):
self.__final_constraints = []
if self.__final_property:
# compile initial (X0) property
# ex: Px => [$Px$]
l_clauses = self.__compile_property(self.__final_property)
# compile numeric form
# ex: [$Px$] => self.__final_constraints = [[7]]
for clause in l_clauses:
self.__final_constraints.append(self.__code_clause(clause))
dim_fin = self.__dim_final
......
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