private static void writeTraceModel(Configuration conf, Dataset ds, int maxLength, int indexFrom, int indexTo,
                                        String filename) throws FileNotFoundException {
        final StringBuilder sb = new StringBuilder();
        sb.append(ConstraintExtractor.plantCaption(conf));
        sb.append("    step: 0.." + (maxLength - 1) + ";\n");
        sb.append("    unsupported: boolean;\n");
        sb.append("FROZENVAR\n    trace: " + indexFrom + ".." + (indexTo - 1) + ";\n");
        sb.append("ASSIGN\n");
        sb.append("    init(step) := 0;\n");
        sb.append("    next(step) := step < " + (maxLength - 1)
                + " ? step + 1 : " + (maxLength - 1) + ";\n");
        sb.append("    init(unsupported) := FALSE;\n");
        sb.append("    next(unsupported) := step = " + (maxLength - 1) + ";\n");

        for (Parameter p : conf.outputParameters) {
            sb.append("    output_" + p.traceName() + " := case\n");
            for (int traceIndex = indexFrom; traceIndex < indexTo; traceIndex++) {
                sb.append("        trace = " + traceIndex + ": case\n");
                final List<Set<Integer>> valuesToSteps = new ArrayList<>();
                for (int i = 0; i < p.valueCount(); i++) {
                    valuesToSteps.add(new TreeSet<>());
                }
                for (int step = 0; step < ds.values.get(traceIndex).size(); step++) {
                    final double value = ds.get(ds.values.get(traceIndex).get(step), p);
                    final int res = p.traceNameIndex(value);
                    valuesToSteps.get(res).add(step);
                }

                // more compact representation
                final List<Pair<Integer, Set<Integer>>> pairs = new ArrayList<>();
                for (int i = 0; i < p.valueCount(); i++) {
                    if (!valuesToSteps.get(i).isEmpty()) {
                        pairs.add(Pair.of(i, valuesToSteps.get(i)));
                    }
                }

                pairs.sort((v1, v2) -> Integer.compare(v2.getRight().size(), v1.getRight().size()));
                pairs.add(pairs.remove(0)); // shift

                for (int i = 0; i < pairs.size(); i++) {
                    final String condition = i == pairs.size() - 1 ? "TRUE"
                            : ("step in " + expressWithIntervals(pairs.get(i).getRight()));
                    sb.append("            " + condition + ": "
                            + pairs.get(i).getLeft() + ";\n");

                }
                sb.append("        esac;\n");
            }
            sb.append("    esac;\n");
        }

        sb.append("DEFINE\n");
        sb.append("    loop_executed := unsupported;\n");

        sb.append(ConstraintExtractor.plantConversions(conf));

        try (PrintWriter pw = new PrintWriter(filename)) {
            pw.println(sb);
        }
    }