ts_slice.cpp File Reference

#include <transition-system/ts_slice.h>
#include <irep2/irep2_utils.h>
#include <algorithm>

Include dependency graph for ts_slice.cpp:

Functions
void	slice_transition_system (transition_systemt &ts)
	Drop the state variables, definitions and inputs that no property, assumption, invariant or back-edge guard depends on.

Function Documentation

slice_transition_system()

void slice_transition_system

(

transition_systemt &

ts

)

Drop the state variables, definitions and inputs that no property, assumption, invariant or back-edge guard depends on.

A backward slice over one iteration is not enough. Nothing in a single step reads a state's value at the back edge, so an ordinary slicer deletes it – and that value is the transition relation, read by the next step. Reaching a state through its head symbol therefore also pulls in its post and init.