handle molecules defined only in query

nusmv.pl

@@ -58,7 +58,6 @@ export_nusmv_stream_reactions(Stream) :-
   findall(
     (Reactants, [], Products, []),
     (
-      % FIXME we do not take care of reversible reactions
       item([kind: reaction, item: Item]),
       reaction(Item, _, Reactants, Products)
     ),
@@ -85,7 +84,15 @@ enumerate_all_molecules(Molecules) :-
   ;
     InfluenceMolecules = []
   ),
-  union(ReactionMolecules, InfluenceMolecules, Molecules).
+  union(ReactionMolecules, InfluenceMolecules, ModelMolecules),
+  (
+    query_mols(QueryMolecules)
+  ->
+    true
+  ;
+    QueryMolecules = []
+  ),
+  union(ModelMolecules, QueryMolecules, Molecules).
 
 
 export_initial_state(Stream, Molecules) :-
@@ -476,11 +483,17 @@ check_ctl_impl(Query, some, NusmvCX, BoolSem, Result) :-
 :- dynamic(trace/1).
 
 
+% stores unknown molecules coming from the query
+:- dynamic(query_mols/1).
+
+
 % care that if Result is instantiated, the predicate might fail before parsing
 % the full output/trace
 check_ctl_impl(Query, all, NusmvCX, BoolSem, Result) :-
   retractall(trace(_)),
-  normalize_query(Query, NQuery),
+  retractall(query_mols(_)),
+  normalize_query(Query, NQuery, Mols),
+  assertz(query_mols(Mols)),
   translate_ctl_for_nusmv(NQuery, NusmvQuery),
   % FIXME better template, in $TMP, check if not existing, etc.
   export_nusmv_file(nusmv, BoolSem),
@@ -628,3 +641,7 @@ parse_nusmv_out_trace(Out) :-
 
 state_string_to_trace(String, Trace) :-
   split_string(String, "\t", "\t", [_ | Trace]).
+
+
+prolog:message(error(unknown_molecule)) -->
+  ['Unknown molecule in query.'].

revision.pl

@@ -19,7 +19,7 @@ revise_model(Query) :-
     'Use theory-revision on the current model to satisfy the query given as
     argument. cf. \\texttt{CCFS05tcsb}.'
   ),
-  normalize_query(Query, NQuery),
+  normalize_query(Query, NQuery, _),
   categorize_query(NQuery, ECTL, UCTL, ACTL),
   nb_setval(need_recheck, false),
   revise_model(ECTL, UCTL, ACTL, [], [], []).
@@ -30,7 +30,6 @@ revise_model(Query) :-
 revise_model([E | ECTL], UCTL, ACTL, Et, Ut, At) :-
   item([kind: option, item: option(nusmv_initial_states: Init)]),
   item([kind: option, item: option(boolean_semantics: Bool)]),
-  write(checking(E)),nl,
   (
     check_ctl_impl(E, Init, no, Bool, true)
   ->
@@ -47,7 +46,6 @@ revise_model([E | ECTL], UCTL, ACTL, Et, Ut, At) :-
 revise_model([], [U | UCTL], ACTL, Et, Ut, At) :-
   item([kind: option, item: option(nusmv_initial_states: Init)]),
   item([kind: option, item: option(boolean_semantics: Bool)]),
-  write(checking(U)),nl,
   (
     check_ctl_impl(U, Init, no, Bool, true)
   ->
@@ -71,7 +69,6 @@ revise_model([], [U | UCTL], ACTL, Et, Ut, At) :-
 revise_model([], [], [A | ACTL], Et, Ut, At) :-
   item([kind: option, item: option(nusmv_initial_states: Init)]),
   item([kind: option, item: option(boolean_semantics: Bool)]),
-  write(checking(A)),nl,
   check_ctl_impl(A, Init, silent, Bool, Result),
   (
     Result = true
@@ -80,10 +77,7 @@ revise_model([], [], [A | ACTL], Et, Ut, At) :-
     % we only consider adding U' and E' when A is fully satisfied, thus moving
     % a step from the A' step of the algorithm to the A step
     % FIXME check At too since self-loops can be added by removing a reaction
-    write(split(Et, Ut)),nl,
     check_and_split(Et, Ut, [], Ett, Utt, [], Eprime, Uprime, [], Init, Bool),
-    write(true(Ett, Utt)),nl,
-    write(false(Eprime, Uprime)),nl,
     revise_model(Eprime, Uprime, ACTL, Ett, Utt, [A | At])
   ;
     print_message(informational, step('A''')),