Files
tla_visualiser/include/trace_viewer_model.h
2025-12-27 02:56:19 +00:00

63 lines
1.7 KiB
C++

#ifndef TRACE_VIEWER_MODEL_H
#define TRACE_VIEWER_MODEL_H
#include <QAbstractListModel>
#include <QObject>
#include <QString>
#include <vector>
#include "tlc_runner.h"
namespace tla_visualiser {
/**
* @brief Qt model for displaying trace/counterexample steps
*
* Provides data for QML trace viewer with step-by-step inspection.
*/
class TraceViewerModel : public QAbstractListModel {
Q_OBJECT
Q_PROPERTY(int stepCount READ stepCount NOTIFY dataChanged)
Q_PROPERTY(int currentStep READ currentStep WRITE setCurrentStep NOTIFY currentStepChanged)
public:
enum Roles {
StepNumberRole = Qt::UserRole + 1,
StateIdRole,
StateDescriptionRole,
ActionRole,
VariablesRole
};
explicit TraceViewerModel(QObject* parent = nullptr);
~TraceViewerModel() override;
// QAbstractListModel interface
int rowCount(const QModelIndex& parent = QModelIndex()) const override;
QVariant data(const QModelIndex& index, int role = Qt::DisplayRole) const override;
QHash<int, QByteArray> roleNames() const override;
// Custom methods
Q_INVOKABLE void loadTrace(const TLCRunner::CounterExample& trace,
const TLCRunner::RunResults& results);
Q_INVOKABLE void clear();
Q_INVOKABLE QVariantMap getStepDetails(int step) const;
Q_INVOKABLE QString exportToMarkdown() const;
Q_INVOKABLE QString exportToJson() const;
int stepCount() const;
int currentStep() const;
void setCurrentStep(int step);
signals:
void currentStepChanged();
void traceUpdated();
private:
class Impl;
std::unique_ptr<Impl> pImpl;
};
} // namespace tla_visualiser
#endif // TRACE_VIEWER_MODEL_H