Commit ca855876 authored by Thierry Martinez's avatar Thierry Martinez

NuSMV

parent e9240da2
......@@ -5,7 +5,7 @@
output_file/1,
filename/2,
chop_suffix/2,
automatic_suffix/3
automatic_suffix/4
]
).
......@@ -45,12 +45,18 @@ chop_suffix(Filename, Suffix) :-
).
automatic_suffix(Filename, DefaultSuffix, FullFilename) :-
automatic_suffix(Filename, DefaultSuffix, Mode, FullFilename) :-
chop_suffix(Filename, Suffix),
(
Suffix = '',
atom_concat(Filename, DefaultSuffix, FullFilename),
exists_file(FullFilename)
(
Mode = read
->
exists_file(FullFilename)
;
true
)
->
true
;
......
......@@ -2,6 +2,7 @@
initial_state,
[
get_initial_state/2,
get_initial_concentration/2,
list_initial_state/0,
clear_initial_state/0,
present/1,
......@@ -14,17 +15,38 @@
).
get_initial_state(Object, Concentration) :-
get_initial_state(Object, State) :-
(
item([model: current_model, kind: initial_state, item: present(Object)])
item([model: current_model, kind: initial_state, key: Object, item: Item])
->
Concentration = 1
(
Item = present(Object)
->
State = present(1)
;
Item = present(Object, Concentration)
->
(
Concentration = 0
->
State = absent
;
State = present(Concentration)
)
;
Item = absent(Object)
->
State = absent
)
;
item([
model: current_model,
kind: initial_state,
item: present(Object, Concentration)
])
State = undefined
).
get_initial_concentration(Object, Concentration) :-
get_initial_state(Object, State),
(
State = present(Concentration)
->
true
;
......
......@@ -110,7 +110,7 @@ add_biocham(InputFile) :-
add_biocham_file(Filename) :-
automatic_suffix(Filename, '.bc', FilenameBc),
automatic_suffix(Filename, '.bc', read, FilenameBc),
file_directory_name(FilenameBc, FileDirectory),
setup_call_cleanup(
(
......
#include <stdio.h>
#include <sbml/SBMLTypes.h>
int
main (int argc, char *argv[])
{
const char *filename;
SBMLDocument_t *document;
Model_t *model;
if (argc != 2) {
fprintf(stderr, "Usage: sbml2biocham filename\n");
return 2;
}
filename = argv[1];
document = readSBML(filename);
if (SBMLDocument_getNumErrors(document) != 0) {
SBMLDocument_printErrors(document, stderr);
return 1;
}
model = SBMLDocument_getModel(document);
SBMLDocument_free(document);
return 0;
}
#include <stdlib.h>
#include <iostream>
#include <sbml/SBMLTypes.h>
int
main (int argc, char *argv[])
{
if (argc != 2) {
std::cerr << "Usage: sbml2biocham filename\n";
return 2;
}
const char *filename = argv[1];
SBMLDocument *document = readSBML(filename);
if (document->getErrorLog()->getNumFailsWithSeverity(LIBSBML_SEV_ERROR)
> 0) {
document->printErrors();
return EXIT_FAILURE;
}
Model *model = document->getModel();
delete document;
return 0;
}
......@@ -65,7 +65,7 @@ gather_initial_values(InitialValues) :-
(
between(0, VariableMax, VariableIndex),
variable(Molecule, VariableIndex),
get_initial_state(Molecule, InitialValue)
get_initial_concentration(Molecule, InitialValue)
),
InitialValues
).
......
:- module(
nusmv,
[
export_nusmv/1
]
).
export_nusmv(OutputFile) :-
biocham_command,
type(OutputFile, output_file),
doc('
exports the current Biocham set of rules and initial state in an SMV
\\texttt{.smv} file.
'),
automatic_suffix(OutputFile, '.smv', write, FilenameSmv),
setup_call_cleanup(
open(FilenameSmv, write, Stream),
export_nusmv_stream(Stream),
close(Stream)
).
no_false_initial_state :-
fail.
export_nusmv_stream(Stream) :-
write(Stream, 'MODULE main\n'),
findall(
(Reactants, Products),
(
item([model: current_model, kind: rule, item: Item]),
rule(Item, _, Reactants, Products)
),
Rules
),
length(Rules, RuleCount),
enumerate_molecules(Molecules),
export_initial_state(Stream, Molecules, RuleCount),
export_rules(Stream, Molecules, Rules).
export_initial_state(Stream, Molecules, RuleCount) :-
write(Stream, 'VAR\n'),
(
no_false_initial_state
->
FirstState = 1
;
FirstState = 0
),
format(Stream, 'R: ~d..~d;\n', [FirstState, RuleCount]),
\+ (
member(Molecule, Molecules),
\+ (
make_nusmv_name(Molecule, Name),
format(Stream, '~a: boolean;\n', [Name])
)
),
(
RuleCount < 2
->
NextStates = '1'
;
format(atom(NextStates), '1..~d', [RuleCount])
),
format(Stream, '\c
ASSIGN
init(R) := ~d;
next(R) := ~a;
', [FirstState, NextStates]).
export_rules(Stream, Molecules, Rules) :-
\+ (
member(Molecule, Molecules),
\+ (
export_molecule_rules(Stream, Molecule, Rules)
)
).
export_molecule_rules(Stream, Molecule, Rules) :-
make_nusmv_name(Molecule, Name),
get_initial_state(Molecule, InitialState),
nusmv_initial_state(InitialState, NusmvInitialState),
format(Stream, '\c
init(~a) := FALSE;
next(~a) := case
R = 0: ~a;
', [Name, Name, NusmvInitialState]),
\+ (
nth1(RuleIndex, Rules, (Reactants, Products)),
\+ (
(
(
member((_ * Molecule), Products)
->
Result = 'TRUE'
;
member((_ * Molecule), Reactants)
->
Result = '{FALSE, TRUE}'
)
->
format(Stream, ' R = ~d: case\n', [RuleIndex]),
findall(
ReactantName,
(
member(_ * Reactant, Reactants),
make_nusmv_name(Reactant, ReactantName)
),
ReactantNames
),
atomic_list_concat(ReactantNames, ' & ', Condition),
format(Stream, ' \c
(~a): ~a;
TRUE: ~a;
esac;
', [Condition, Result, Name])
)
;
true
)
),
format(Stream, ' \c
TRUE: ~a;
esac;
', [Name]).
nusmv_initial_state(present(_), 'TRUE').
nusmv_initial_state(absent, 'FALSE').
nusmv_initial_state(undefined, '{FALSE, TRUE}').
make_nusmv_name(Molecule, Name) :-
reserved(Molecule),
!,
atom_concat('_', Molecule, Name).
make_nusmv_name(Molecule, Name) :-
atom_chars(Molecule, MoleculeChars),
findall(
TranslatedChar,
(
member(Char, MoleculeChars),
(
once(translate_char(Char, TranslatedChar))
;
TranslatedChar = Char
)
),
TranslatedList
),
atomic_list_concat(TranslatedList, Name).
translate_char('_', '__').
translate_char(',', '_c').
translate_char('~', '_l').
translate_char('(', '_L').
translate_char(')', '_R').
translate_char('{', '_l').
translate_char('}', '_r').
reserved('B').
reserved('F').
reserved('G').
reserved('H').
reserved('O').
reserved('S').
reserved('T').
reserved('V').
reserved('W').
reserved('X').
reserved('Y').
reserved('Z').
reserved('A').
reserved('E').
reserved('U').
reserved('AF').
reserved('EF').
reserved('AG').
reserved('EG').
reserved('AX').
reserved('EX').
reserved('xor').
reserved('R').
:- use_module(library(plunit)).
:- begin_tests(nusmv).
test('nusmv') :-
new_model,
add_rule(a => b),
add_rule(a + b => c),
command(present(a)),
command(absent(c)),
export_nusmv('unittest').
:- end_tests(nusmv).
......@@ -65,8 +65,8 @@ print_ode :-
write('Init \tODE\n'),
\+ (
ode(Molecule, Equation),
get_initial_state(Molecule, InitialState),
get_initial_concentration(Molecule, InitialConcentration),
\+ (
format('~f \td[~w]/dt=~w\n', [InitialState, Molecule, Equation])
format('~f \td[~w]/dt=~w\n', [InitialConcentration, Molecule, Equation])
)
).
......@@ -273,3 +273,13 @@ enumerate_molecule(Molecule) :-
;
member(_ * Molecule, Products)
).
enumerate_molecule(Molecule) :-
item([model: current_model, kind: initial_state, item: Item]),
(
Item = present(Molecule)
;
Item = present(Molecule, _Concentration)
;
Item = absent
).
......@@ -35,6 +35,8 @@
*** ODE files
*** Graphics files
*** Other files
- nusmv.pl
- nusmv.plt
** Listing and editing rules and events
*** Rules
- rule_editor.pl
......
......@@ -27,7 +27,7 @@ load_trace(InputFile) :-
\+ (
filename(InputFile, Filename),
\+ (
automatic_suffix(Filename, '.csv', FilenameCsv),
automatic_suffix(Filename, '.csv', read, FilenameCsv),
csv_read_file(FilenameCsv, Data),
add_trace(FilenameCsv, Data)
)
......@@ -42,7 +42,7 @@ save_trace(OutputFile) :-
nb_getval(current_trace, Id),
find_item([key: Id, item: Data]),
once(filename(OutputFile, Filename)),
automatic_suffix(Filename, '.csv', FilenameCsv),
automatic_suffix(Filename, '.csv', write, FilenameCsv),
csv_write_file(FilenameCsv, Data).
......
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