informalsystems / modelator-py

Utilities for the TLA+ ecoystem and model-based testing using TLA+.
Apache License 2.0
28 stars 2 forks source link

Feature: implement a better prototype trace subset selection function #36

Open danwt opened 2 years ago

danwt commented 2 years ago

Context

There is an extremely basic unoptimized version here

https://github.com/informalsystems/modelator-py/blob/bc71f46f0e0cfe85843c63d46c590fce51cbd0fb/modelator/scratch_subset_selection.py

, which could be replaced by a more optimized version using some efficient array encoding, by for example using numpy.

A real long term implementation should probably be done in Rust.