1		:- module(ltsmin_trace, [csv_to_trace/3]).
2
3		:- use_module(library(lists)).
4		:- use_module(library(fastrw)).
5		:- use_module(probsrc(tools), [split_chars/3, split_complex_sep/3]).
6		:- use_module(probsrc(error_manager), [add_internal_error/2]).
7
8		:- use_module(extension('ltsmin/ltsmin_c_interface'), [read_hex_str/2, free_str/1, loadfr/0,atom_charptr/2]).
9		:- use_module(extension('ltsmin/ltsmin'), [generate_bindings/3]).
10
11		:- set_prolog_flag(double_quotes, codes).
12
13
14		read_all_lines(Acc, R) :-
15		read_line(L),
16		(L == end_of_file
17		-> Acc = R
18		; read_all_lines([L|Acc], R)).
19
20
21		read_trace(Filename, TypeInfo, Lines, ButLastLines) :-
22		open(Filename, read, Stream),
23		see(Stream),
24		read_all_lines([], ReversedLines),
25		seen,
26		(ReversedLines = [_LastLine|ButLastLinesRev]
27		->
28		reverse(ReversedLines, [TypeInfo|Lines]),
29		reverse(ButLastLinesRev, [TypeInfo|ButLastLines])
30		; add_internal_error('LTSmin trace file is empty: ',Filename),fail).
31
32
33		%% HACK: some values are not pretty printed into the #hexcode# representation
34		%% TODO: either fix LTSmin to do so or handle these cases separately (pk, 30.11.2017)
35		fast_buf_hex_to_term("\"D]\"", []) :- !.
36		fast_buf_hex_to_term(HexStr, Term) :-
37		read_hex_str(HexStr, Tmp),
38		fast_buf_read(Term, Tmp),
39		free_str(Tmp).
40
41
42
43		line_to_state(VariableList, Line, State) :-
44		split_complex_sep(Line, ",,", Vals), % NOTE: this explictly split on a single comma beforehand. But that seems wrong.
45		length(VariableList, Len),
46		length(BinState, Len),
47		prefix(Vals, BinState),
48		maplist(fast_buf_hex_to_term, BinState, UnboundState),
49		generate_bindings(UnboundState, VariableList, State),!.
50		line_to_state(_VariableList, Line, _State) :-
51		add_internal_error('Could not extract state from LTSmin trace line: ',Line),fail.
52
53		butlast(L, BL) :-
54		reverse(L, [_Last|Rev]),
55		reverse(Rev, BL).
56
57		extract_op(Line, Op) :-
58		split_complex_sep(Line, ",,", Vals),
59		reverse(Vals, [QuotedOpCodesFRW|_]),
60		butlast(QuotedOpCodesFRW, [_|OpCodesFRW]),
61		atom_charptr(OpCodesFRW, OpFRW),
62		fast_buf_read(Op, OpFRW),
63		free_str(OpFRW),!.
64		extract_op(Line, _Op) :-
65		add_internal_error('Could not extract operation from LTSmin trace line: ',Line),fail.
66
67		:- meta_predicate take_while(1,*,*).
68		:- meta_predicate take_while1(*,1,*).
69		take_while(Pred, List, Res) :-
70		take_while1(List, Pred, Res).
71		take_while1([], _, []).
72		take_while1([H|T], Pred, R) :-
73		(call(Pred, H)
74		-> R = [H|RT], take_while1(T, Pred, RT)
75		; R = []).
76
77
78		starts_with(Pre, Str) :-
79		append(Pre, _, Str).
80
81		split_at_colon(S, L, R) :-
82		split_chars(S, ":", [L, R]).
83
84		extract_variable_list(TypeInfoLine, Variables, _Types) :-
85		split_complex_sep(TypeInfoLine, ",,", TypeInfo),
86		take_while(starts_with("DA"), TypeInfo, TypedVariables),
87		maplist(split_at_colon, TypedVariables, DAVariables, _TypesAsStrings),
88		maplist(append("DA"), VariablesStrs, DAVariables),
89		maplist(atom_codes, Variables, VariablesStrs).
90
91		csv_to_trace(FileName, StateList, ['$init_state'|OpList]) :-
92		loadfr,
93		read_trace(FileName, TypeInfo, [DummyState|Lines], [DummyState|ButLastLines]),
94		extract_variable_list(TypeInfo, VariableList, _TypeList),
95		extract_op(DummyState, '$init_state'),
96		maplist(line_to_state(VariableList), Lines, StateList),
97		maplist(extract_op, ButLastLines, OpList).