Merge branch 'develop' into feature/Hybrid

.gitignore

@@ -6,8 +6,6 @@ platform/current
 modules/graphviz/graphviz_swiprolog
 modules/partialfrac/roots
 modules/sbml/sbml_swiprolog
-modules/glucose/glucose-syrup
-modules/glucose/glucose_swiprolog
 swipl-biocham
 Untitled*.ipynb
 .ipynb_checkpoints
@@ -38,4 +36,3 @@ biocham_jupyter/guinbextension/package-lock.json
 *.py~
 *.pyc
 .DS_Store
-modules/glucose/patch.done

.gitlab-ci.yml

@@ -39,10 +39,14 @@ pages:
         - linux
     script:
         - make doc/index.html web/biocham.zip
+        - curl --fail "$CI_PAGES_URL/content.zip" -o content.zip
+        - if [ -r content.zip ]; then unzip content.zip; rm content.zip; fi
         - mkdir -p public
         - cp -r doc devdoc web/*.{html,png,zip} public
         - if [[ -n "$CI_COMMIT_TAG" ]] ; then cp public/biocham.zip public/biocham_$CI_COMMIT_TAG.zip ; mv public/doc public/doc_$CI_COMMIT_TAG ; ln -s doc_$CI_COMMIT_TAG public/doc ; fi
         - cp public/biocham.zip public/biocham_latest.zip
+        - zip -r content.zip public
+        - mv content.zip public
     artifacts:
         paths:
             - public

Makefile

@@ -2,8 +2,7 @@
 
 ADDITIONAL_MODULES= \
   modules/sbml/sbml_utils.pl \
-  modules/partialfrac/partialfraction.pl \
-  modules/glucose/glucose.pl
+  modules/partialfrac/partialfraction.pl
 MODULES=$(shell sed -n -E 's/^[+-] (.*\.pl)$$/\1/p' toc.org) \
   $(ADDITIONAL_MODULES)
 # load_test_files/1 should make this useless, but I cannot find how to use it
@@ -29,9 +28,7 @@ ifeq ($(SWIPL_GE_7713),true)
 endif
 SUBDIRS=$(dir $(wildcard modules/*/Makefile))
 
-# glucose source needs its own header files
-INCLUDEDIRS=$(PLBASE)/include $(SUBDIRS) \
-  modules/glucose/glucose-syrup modules/glucose/glucose-syrup/core
+INCLUDEDIRS=$(PLBASE)/include $(SUBDIRS)
 
 RPATH=
 ifneq ($(LD_RUN_PATH),)
@@ -56,12 +53,17 @@ JUPYTER_DIR=$(CURDIR)/biocham_jupyter
 KERNEL_DIR=$(JUPYTER_DIR)/kernel/biocham_kernel
 WORKFLOWS_DIR=$(JUPYTER_DIR)/guinbextension/src/config/workflows
 
+# NOTEBOOKS=$(shell find . -type f -name '*.ipynb' -print)
+NOTEBOOKS=library/examples/doctor_in_the_cell/diagnosis.ipynb library/examples/tutorial/tutorial17cmsb.ipynb
+REFDIR=nbhtml
+
 all: biocham biocham_debug test doc/index.html pldoc install_kernel install_gui
 
 quick: unit_tests
 
 .PHONY: all slow test unit_tests clean web cabernet cabernet_restart \
-  install_kernel gadagne gadagne_restart jupyter_tests install pldoc devdoc
+  install_kernel gadagne gadagne_restart jupyter_tests install pldoc devdoc \
+  refs
 
 install: biocham biocham_debug
 	mkdir -p $(PREFIX)/bin
@@ -91,16 +93,10 @@ biocham_debug: $(SWIPL) $(MODULES) $(TEST_MODULES) toc.org $(CMAES_LIB) \
 $(SWIPL): $(SWIPL).c \
 		modules/graphviz/graphviz_swiprolog.c \
 		modules/sbml/sbml_swiprolog.c \
-		modules/partialfrac/roots.c \
-		modules/glucose/glucose_swiprolog.cc \
-		modules/glucose/glucose-syrup/core/Solver.cc
+		modules/partialfrac/roots.c
 	for dir in $(SUBDIRS) ; do $(MAKE) -C $$dir ; done
 	$(CXX) $(CXXFLAGS) $^ $(LDFLAGS) $(LDLIBS) -lstdc++ -o $@
 
-# FIXME should be unnecessary once cache works on CI
-modules/glucose/glucose-syrup/core/Solver.cc:
-	cp -r /tmp/glucose-syrup modules/glucose/
-
 doc/index.html doc/commands.js: biocham
 	./biocham --generate-doc
 
@@ -126,16 +122,16 @@ test_%: biocham_debug
 	echo "flag(slow_test, _, true), run_tests_and_halt('$*')." | ./biocham_debug
 
 install_kernel: biocham $(KERNEL_DIR)/commands.js $(KERNEL_DIR)/commands.py $(WORKFLOWS_DIR)/workflows.js
-	- pip3 install --user $(JUPYTER_DIR)/kernel
+	- pip3 install --user $(JUPYTER_DIR)/kernel || pip install --user $(JUPYTER_DIR)/kernel
 	- jupyter kernelspec install --user --name=biocham $(KERNEL_DIR)
 
 install_gui: $(WORKFLOWS_DIR)/workflows.js
-	- cd $(JUPYTER_DIR)/guinbextension && npm run build && npm run docs:build
+	- cd $(JUPYTER_DIR)/guinbextension && npm install && npm run build && npm run docs:build
 	- jupyter nbextension install --user $(JUPYTER_DIR)/guinbextension/gui-build/
 	- jupyter nbextension enable --user gui-build/nbextension
 
 install_gui_dev: $(WORKFLOWS_DIR)/workflows.js
-	- cd $(JUPYTER_DIR)/guinbextension && npm run dev && npm run docs:build
+	- cd $(JUPYTER_DIR)/guinbextension && npm install && npm run dev && npm run docs:build
 	- jupyter nbextension install --user $(JUPYTER_DIR)/guinbextension/gui-build/
 	- jupyter nbextension enable --user gui-build/nbextension
 
@@ -150,9 +146,9 @@ $(KERNEL_DIR)/commands.py: biocham
 $(KERNEL_DIR)/commands.js: doc/commands.js
 	cp -f $< $@
 
+# only static .bc files in that dir
 $(WORKFLOWS_DIR)/workflows.js: 
-	for file in $(WORKFLOWS_DIR)/nb/*.ipynb ; do \
-		if test -f $$file; then jupyter nbconvert --to script $$file ; fi ; done
+	# for file in $(WORKFLOWS_DIR)/nb/*.ipynb ; do jupyter nbconvert --to script $$file ; done
 	python3 $(WORKFLOWS_DIR)/make_workflows.py -i $(WORKFLOWS_DIR)/nb/ -o $@
 
 clean:
@@ -204,7 +200,22 @@ gadagne_restart: gadagne
 release:
 	@read -p "Version number (e.g. 4.1.0): " version && \
 	sed -i'' -e "s/^version('.*')/version('$$version')/" about.pl && \
+	sed -i'' -e "s/\"version\": \"\(.*\)\"/\"version\": \"$$version\"/" biocham_jupyter/guinbextension/package.json && \
+	sed -i'' -e "s/__version__ = '\(.*\)'/__version__ = '$$version'/" biocham_jupyter/kernel/biocham_kernel/__init__.py && \
 	LC_ALL=C sed -i'' -e "s+^<h1>version.*</h1>+<h1>version $$version $(shell date '+%B %Y')</h1>+" web/index.html && \
 	git commit about.pl web/index.html -m "Version $$version" && \
 	git tag -a v$$version -m "Version $$version" && \
 	git push --tags
+
+refs: $(NOTEBOOKS) biocham
+	mkdir -p $(REFDIR)
+	jupyter nbconvert --ExecutePreprocessor.timeout=None \
+		--to html --output-dir $(REFDIR) --execute $(NOTEBOOKS)
+	for file in $(NOTEBOOKS) ; do \
+		out=$(REFDIR)/$$(basename $${file%%ipynb}html) && \
+		if [ -f $$out.ref ] ; then \
+			diff -q $$out $$out.ref || false ; break ; \
+		else \
+			cp $$out $$out.ref ; \
+		fi ; \
+	done

README.md

@@ -8,12 +8,17 @@ After `git clone` you might need to run once the [install.sh](./install.sh)
 script in order to install all build dependencies and to try to compile the
 project.
 
-After that `make` wiill build the whole project, including documentation,
+After that `make` will build the whole project, including documentation,
 tests, debug version, etc., which might be quite slow.
 You might want to use `make biocham`, `make biocham_debug` (a SWI-Prolog
 toplevel with all biocham files loaded) or `make test_<unit>` (to run a single
 test unit) for faster feedback.
 
+Note that `make test` will give you, if available, some test coverage
+estimation, and that `make test_<unit>` will attempt to get into more details
+about which clauses were not covered (but this highly depends on the SWIPL
+version).
+
 ## Documentation
 
 The file [toc.org](./toc.org) is used for three things:

about.pl

@@ -8,7 +8,7 @@
     about/0
   ]).
 
-version('4.1.29').
+version('4.2.6').
 
 copyright(
   'Copyright (C) 2003-2019 Inria, EPI Lifeware, Saclay-Île de France, France'

biocham.pl

@@ -25,7 +25,7 @@ The Biochemical Abstract Machine (Biocham) is a modelling software for cell syst
   software.').
 
 :- doc('
-This reference manual (as its extended version for developpers) is automaticaly generated from the source code of Biocham.').
+This reference manual (as its extended version for developers) is automatically generated from the source code of Biocham.').
 
 :- doc('
 Biocham v4 is mainly composed of :

biocham_jupyter/guinbextension/package.json

 {
   "name": "gui",
-  "version": "4.1.29",
+  "version": "4.2.6",
   "description": "biocham gui in jupyter notebook",
   "main": "src/index.js",
   "scripts": {

biocham_jupyter/guinbextension/src/config/workflows/commands.py

@@ -153,6 +153,7 @@ commands = [
     "option",
     "pac_learning",
     "parameter",
+    "pattern_reduction",
     "place",
     "plot",
     "present",

biocham_jupyter/kernel/biocham_kernel/__init__.py

 """Example magic"""
-__version__ = '4.1.29'
+__version__ = '4.2.6'

doc.pl

@@ -16,7 +16,6 @@
   ]
 ).
 
-
 doc(_) :- % this predicate must just succeed in prolog
   !,
   true.
@@ -102,7 +101,6 @@ format_doc_html(document_opening(Title)) :-
 <head>
   <meta charset="UTF-8">
   <title>~a</title>
-</head>
 <style>
   h5 {font-family: "Courier New"; font-size: 1.1em; font-weight: normal; }
   div.indented {margin-left: 1cm; }
@@ -121,14 +119,21 @@ format_doc_html(document_opening(Title)) :-
   blockquote.SS {color : orange; }
   blockquote.TM {color : green; }
 </style>
+</head>
 <body>
+<header>
   <h1><img src="logo.png" alt="logo.png">~a</h1>
-  <h2>Inria <a href=~a>~a</a></h2>
+  <h2>Inria <a href="~a">~a</a></h2>
+</header>
 ', [Title, Url, Url]).
 
 format_doc_html(table_of_contents) :-
   !,
-  format('  <h2 id="Contents">Contents</h2>\n', []).
+  format('  <nav>~n  <h2 id="Contents">Contents</h2>\n', []).
+
+format_doc_html(end_table_of_contents) :-
+  !,
+  format('  </nav>~n  <main>', []).
 
 format_doc_html(toc_entry(Id, Title)) :-
   !,
@@ -180,7 +185,7 @@ format_doc_html(chapter(Id, Counter, Title)) :-
     true
   ),
   format(CommandsStream, '   {kind: "chapter", name: "~w"}', [Title]),
-  format('<h2 id="~a">Chapter ~d</br>~a</h2>', [Id, Counter, Title]).
+  format('<h2 id="~a">Chapter ~d<br>~a</h2>', [Id, Counter, Title]).
 
 format_doc_html(section(HLevel, Id, Title)) :-
   !,
@@ -325,18 +330,20 @@ format_doc_html(html(Html)) :-
 format_doc_html(document_closing) :-
   !,
   format('
+  </main>
 </body>
 </html>
 ', []).
 
 format_doc_html(begin_grammar(Id, Grammar)) :-
-  format('<div><table id="~a"><td>~a ::= </td><td>\n', [Id, Grammar]).
+  format('<div><table id="~a"><tr><td>~a ::= </td><td>\n', [Id, Grammar]).
 
+% FIXME operators are not escaped and it is a nightmare to fix
 format_doc_html(grammar_item(Item)) :-
   format('<div>| <code>~w</code></div>', [Item]).
 
 format_doc_html(end_grammar) :-
-  format('</td></table></div>\n', []).
+  format('</td></tr></table></div>\n', []).
 
 format_doc_html(begin_command(Id, Command)) :-
   nb_getval(doc_commands_stream, CommandsStream),
@@ -540,6 +547,9 @@ format_doc_tex(table_of_contents) :-
   !,
   format('  \\tableofcontents\n', []).
 
+format_doc_tex(end_table_of_contents) :-
+  !.
+
 format_doc_tex(toc_entry(_Id, _Title)) :-
   !.
 
@@ -897,12 +907,14 @@ setup_doc :-
 
 generate_doc :-
   setup_doc,
-  generate_doc_file(doc).
+  generate_doc_file(doc),
+  check_doc(doc, quiet).
 
 
 generate_devdoc :-
   setup_doc,
-  generate_doc_file(devdoc).
+  generate_doc_file(devdoc),
+  check_doc(devdoc, quiet).
 
 
 generate_doc_file(Type) :-
@@ -979,7 +991,8 @@ generate_toc(Type) :-
       generate_toc_section(Level, Title)
     )
   ),
-  goto_toc_level(0).
+  goto_toc_level(0),
+  format_doc(end_table_of_contents).
 
 
 generate_toc_section(1, Title) :-
@@ -2241,3 +2254,32 @@ clean_doc(Doc, Clean) :-
   atomics_to_string(List1, "\\\"", QuotedString),
   split_string(QuotedString, "\s\t\n", "\s\t\n", List),
   atomics_to_string(List, ' ', Clean).
+
+
+check_doc(Dir, Errors) :-
+  directory_file_path(Dir, 'index.html', Path),
+  load_html(Path, Dom, [syntax_errors(Errors)]),
+  % images
+  forall(
+    (
+      sub_term(element(img, Attrs, []), Dom),
+      memberchk(src=Link, Attrs)
+    ),
+    (
+      directory_file_path(Dir, Link, File),
+      access_file(File, read)
+    )
+  ),
+  % links
+  forall(
+    (
+      sub_term(element(a, Attrs, _), Dom),
+      memberchk(href=Link, Attrs),
+      \+ atom_concat('#', _, Link),
+      \+ atom_concat('http', _, Link)
+    ),
+    (
+      directory_file_path(Dir, Link, File),
+      access_file(File, read)
+    )
+  ).

glucose.py

+#!/usr/bin/env python3
+# -*- coding: utf-8 -*-
+
+"""Emulate glucose command line with python-sat module."""
+
+import argparse
+import sys
+
+from pysat.formula import CNF
+from pysat.solvers import Glucose4
+
+
+def main(infile, outfile):
+    """Call glucose v4.1 with infile and write output to outfile."""
+    with Glucose4(bootstrap_with=CNF(from_file=infile).clauses) as s:
+        if s.solve():
+            print(" ".join(map(str, s.get_model())), "0", file=outfile)
+        else:
+            print("UNSAT", file=outfile)
+
+
+if __name__ == "__main__":
+    parser = argparse.ArgumentParser(description=sys.modules[__name__].__doc__)
+    parser.add_argument(
+        "infile", type=argparse.FileType("r"), help="CNF input file in DIMACS format"
+    )
+    parser.add_argument(
+        "outfile", type=argparse.FileType("w"), help="UNSAT or solution in DIMACS style"
+    )
+    arguments = parser.parse_args(sys.argv[1:])
+    main(arguments.infile.name, arguments.outfile)

gpac.plt

@@ -33,10 +33,21 @@ test(compute_number_species) :-
    gpac:compute_number_species([0,3,0,1,0],8,3),
    gpac:compute_number_species([2,2,0],9,1).
 
-test(generate_variable) :-
-   gpac:generate_variable([3,1],7,[[1,0],[2,0],[3,0],[0,1],[1,1],[2,1],[3,1]]),
-   gpac:generate_variable([2,2],8,[[1,0],[2,0],[0,1],[1,1],[2,1],[0,2],[1,2],[2,2]]),
-   gpac:generate_variable([0,2,0,1],7,[[1,0,0,0],[0,0,1,0],[0,1,0,0],[0,2,0,0],[0,0,0,1],[0,1,0,1],[0,2,0,1]]).
+test(generate_sufficient_variables1) :-
+   PODE = [[[1,[1, 1]],[3,[0, 1]]],[[-1,[3, 0]]]],
+   gpac:generate_sufficient_variables(PODE,Set),
+   once(permutation(Set, [[1,0],[0,1],[2,0],[1,1],[3,0],[2,1]])).
+
+test(generate_sufficient_variables2) :-
+   PODE = [[[1,[3, 1]]],[[-1,[1, 3]]]],
+   gpac:generate_sufficient_variables(PODE,Set),
+   once(permutation(Set, [[1,0],[0,1],[2,0],[1,1],[0,2],[3,0],[1,2],[2,1],[0,3],
+   [3,1],[2,2],[1,3],[3,2],[2,3]])).
+
+test(generate_sufficient_variables3) :-
+   PODE = [[[1,[0, 3]]],[[-1,[0, 2]]]],
+   gpac:generate_sufficient_variables(PODE,Set),
+   once(permutation(Set, [[1,0],[0,1],[0,2]])).
 
 test(reduce_to_binomial_nomodif) :-
    once(gpac:reduce_to_binomial([2,[[[1,[1, 1]]],[[-1,[1, 0]]]],[1,2]],P)),
@@ -51,23 +62,50 @@ test(scan_order_multivar) :-
    gpac:scan_order_multivar([[1,[1, 2]],[1,[1, 1]]],3),
    gpac:scan_order_multivar([[1,[1, 2]],[1,[12, 1]]],13).
 
-test(add_new_variable_monomial) :-
-   gpac:add_new_variable_monomial([1,[1,1,1]],[1,0,1],[1,[0,1,0,1]]),
-   gpac:add_new_variable_monomial([2,[1,1,0]],[1,0,1],[2,[1,1,0,0]]),
-   gpac:add_new_variable_monomial([2,[2,1,3]],[1,0,1],[2,[0,1,1,2]]).
+test(add_all_sons) :-
+   gpac:add_all_sons([a, b],[a, b, c],[],[[a, b, c]]),
+   gpac:add_all_sons([a],[a, b, c],[[a, c]],[[a, b]]),
+   gpac:add_all_sons([a],[a, b, c],[],[[a, b], [a, c]]).
 
-test(add_new_variable) :-
-   PODE = [ [[1,[0,1]],[2,[1,1]]] , [[3,[1,0]]] ],
-   Modified_PODE = [[[1,[0,1,0]],[2,[0,0,1]]],[[3,[1,0,0]]],[[3,[2,0,0]],[1,[0,2,0]],[2,[0,1,1]]]],
-   gpac:add_new_variable([2,PODE,[1,2]],[1,1],[3,Modified_PODE,[1,2,2]]).
+%%% Test of PIVP manipulation %%%
 
-test(compute_derivative) :-
+test(compute_derivative1) :-
    PODE = [ [[1,[0,1]],[2,[1,1]]] , [[3,[1,0]]] ],
-   gpac:compute_derivative([1,1],PODE,1,[[3,[2,0]],[1,[0,2]],[2,[1,2]]]).
+   gpac:compute_derivative([1,1], PODE, Deriv),
+   once(permutation(Deriv, [[3,[2,0]],[1,[0,2]],[2,[1,2]]])).
+
+test(compute_derivative2) :-
+   PODE = [ [[1,[0,1,0]]] , [[3,[1,0,0]],[2,[1,1,0]]] , [[-2,[1,1,0]]] ],
+   gpac:compute_derivative([0,1,1], PODE, Deriv),
+   once(permutation(Deriv, [[3,[1,0,1]],[2,[1,1,1]],[-2,[1,2,0]]])).
+
+test(compute_derivative3) :-
+   PODE = [ [[1,[0,1,0]]] , [[3,[0,2,0]]] , [[-2,[0,1,1]]] ],
+   gpac:compute_derivative([0,1,1], PODE, Deriv),
+   once(permutation(Deriv, [[1,[0,2,1]]])).
+
+test(invert_PIVP) :-
+   gpac:exp_PIVP(Exp),
+   ResPIVP = [2,[[[-1,[2,1]]],[[1,[0,1]]]],[1,1]],
+   gpac:invert_PIVP(Exp, ResPIVP).
+
+test(add_PIVP) :-
+   PIVP1 = [1, [ [ [1, [1]] ] ], [1]],
+   PIVP2 = [1, [ [ [-1, [2]] ] ], [1]],
+   gpac:add_PIVP(PIVP1, PIVP2, PIVP12),
+   PIVP12 = [3,[[[-1,[0,0,2]],[1,[0,1,0]]],[[1,[0,1,0]]],[[-1,[0,0,2]]]],[2,1,1]].
+
+test(multiply_PIVP) :-
+   PIVP1 = [1, [ [ [1, [1]] ] ], [1]],
+   PIVP2 = [1, [ [ [-1, [2]] ] ], [1]],
+   gpac:multiply_PIVP(PIVP1, PIVP2, PIVP12),
+   PIVP12 = [3,[[[1,[0,1,1]],[-1,[0,1,2]]],[[1,[0,1,0]]],[[-1,[0,0,2]]]],[1,1,1]].
 
 test(clean_writing) :-
    gpac:clean_writing(1.0*2, 2),
    gpac:clean_writing(0.0*2, 0),
-   gpac:clean_writing(1.0*input, input).
+   gpac:clean_writing(1.0*input, input),
+   gpac:clean_writing(input^1, input),
+   gpac:clean_writing(input^2, input^2).
 
 :- end_tests(gpac).

influence_properties.pl

@@ -10,13 +10,11 @@
   ]
 ).
 
-:- use_module(library(assoc)).
-:- use_module(library(ordsets)).
-
 % Only for separate compilation/linting
 :- use_module(doc).
 :- use_module(influence_rules).
-
+:- use_module(sat).
+:- use_module(util).
 
 :- doc('The following commands refer to the Boolean dynamics of BIOCHAM models which can be either positive (i.e. without negation, the inhibitors are ignored)
 or negative (the inhibitors of a reaction or an influence are interpreted as negative conditions) \\cite{FMSR16cmsb}.').
@@ -36,9 +34,9 @@ list_stable_states :-
   ),
   list_stable_states(BoolSem),
   forall(
-    stable_state(State),
+    stable_state(NState),
     (
-      write_bool_state(State),
+      write_bool_state(NState),
       nl
     )
   ).
@@ -47,28 +45,35 @@ list_stable_states :-
 :- dynamic(stable_state/1).
 
 
+%! list_stable_states(+BoolSem)
+%
+% Compute stable states for the given BoolSem semantics by calling a SAT
+% solver iteratively and storing solutions in stable_state/1
+%
+% @arg BoolSem positive/negative semantics for influences
 list_stable_states(BoolSem) :-
   retractall(stable_state(_)),
   with_influence_model(influence_properties:(
+    format(atom(Comment), "list stable states (~w)", [BoolSem]),
     mark_subsumed_influences(BoolSem),
-    enumerate_objects(Objects),
-    create_bool_assoc(Objects, BoolState),
-    add_stable_constraints(BoolState, BoolSem),
-    assoc_to_values(BoolState, Bools),
+    write_sat_file(Comment, FileName, Stream),
+    add_stable_constraints(BoolSem),
+    close(Stream),
+    run_sat_iteratively(FileName, Solutions),
     forall(
-      labeling(Bools),
-      assertz(stable_state(BoolState))
+      member(Solution, Solutions),
+      assertz(stable_state(Solution))
     )
-  )),!.
-
-% if there's a failure when adding constraints, we just do nothing
-list_stable_states(_) :-
-  true.
-
+  )),
+  !.
 
 :- dynamic(candidate/1).
 
 
+%! list_tscc_candidates
+%
+% Compute TSCC candidates by calling a SAT solver iteratively and storing
+% solutions in candidate/1
 list_tscc_candidates :-
   biocham_command,
   doc('
@@ -80,20 +85,23 @@ list_tscc_candidates :-
   statistics(walltime, _),
   with_influence_model(influence_properties:(
     mark_subsumed_influences(positive),
-    enumerate_objects(Objects),
-    create_bool_assoc(Objects, BoolState),
-    add_tscc_constraints(BoolState),
-    add_reversibility_constraints(BoolState),
-    assoc_to_values(BoolState, Bools),
+    write_sat_file('list tscc candidates', FileName, Stream),
+    add_tscc_constraints,
+    debug(tscc, "tscc constraint added", []),
+    add_reversibility_constraints,
+    debug(tscc, "reversibility constraint added", []),
+    close(Stream),
+    run_sat_iteratively(FileName, Solutions),
+    debug(tscc, "solutions: ~w", [Solutions]),
     forall(
-      labeling(Bools),
+      member(Solution, Solutions),
       (
         (
-          has_enabled_effective('-', BoolState, _)
+          has_enabled_effective('-', Solution)
         ->
-          assertz(candidate(BoolState))
+          assertz(candidate(Solution))
         ;
-          write_bool_state(BoolState),
+          write_bool_state(Solution),
           write(' stable\n')
         )
       )
@@ -107,8 +115,33 @@ list_tscc_candidates :-
   write('Time: '), write(Time),nl.
 
 
+%! write_sat_file(+Comment, -FileName, -Stream)
+%
+% Create a temporary file, write a temporary header to it, setting up the
+% sat_vars fact with the number of variables, the sat_clauses counter to -1
+% (will be bumped to 0 on writing the header and increased at each
+% write_clause call) and the sat_comment fact to Comment. Also create an alias
+% infl_property_out_stream for the stream for ease of use in write_clause/2
+%
+% @arg Comment    the atom to we put on the first 'c ...' line of the file
+% @arg FileName   the name of the created temporary file
+% @arg Stream     the corresponding stream
+write_sat_file(Comment, FileName, Stream) :-
+    enumerate_objects(Objects),
+    length(Objects, NVar),
+    associate_number_to_objects(Objects),
+    tmp_file_stream(text, FileName, Stream),
+    retractall(sat_comment(_)),
+    assertz(sat_comment(Comment)),
+    retractall(sat_vars(_)),
+    assertz(sat_vars(NVar)),
+    set_counter(sat_clauses, -1),
+    write_sat_header(Stream),
+    set_stream(Stream, alias(infl_property_out_stream)).
+
+
 % all outgoing influences do not change the state
-add_stable_constraints(BoolState, BoolSem) :-
+add_stable_constraints(BoolSem) :-
   findall(
     (PositiveInputs, NegativeInputs, Sign, Output),
     (
@@ -130,11 +163,11 @@ add_stable_constraints(BoolState, BoolSem) :-
     ),
     InfluenceQuads
   ),
-  add_stable_constraint(InfluenceQuads, BoolState).
+  add_stable_constraint(InfluenceQuads).
 
 
 % all outgoing positive influences do not change the state
-add_tscc_constraints(BoolState) :-
+add_tscc_constraints :-
   findall(
     (PositiveInputs, [], Sign, Output),
     (
@@ -149,18 +182,11 @@ add_tscc_constraints(BoolState) :-
     ),
     InfluenceQuads
   ),
-  add_stable_constraint(InfluenceQuads, BoolState).
+  add_stable_constraint(InfluenceQuads).
 
 
 % all outgoing negative influences can be reversed
-%