| summaryrefslogtreecommitdiff |
diff options
| author | Nathanael Sensfelder <SpamShield0@MultiAgentSystems.org> | 2017-07-19 14:32:12 +0200 |
|---|---|---|
| committer | Nathanael Sensfelder <SpamShield0@MultiAgentSystems.org> | 2017-07-19 14:32:12 +0200 |
| commit | 126fb20387caffaa8e05e2a5fee1be78ab1cb1ff (patch) | |
| tree | 81771577766c34497f7f100c955c607debaec041 | |
| parent | c368dd6867fc14463a0f35672a5a7f38693474ed (diff) | |
Dammit, it says flip-flops are combinational...
| -rw-r--r-- | data/property/combinational_processes.pro | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/data/property/combinational_processes.pro b/data/property/combinational_processes.pro index 9300672..7f8405f 100644 --- a/data/property/combinational_processes.pro +++ b/data/property/combinational_processes.pro @@ -2,7 +2,7 @@ ( (ps process STRUCT_COMBINATIONAL_PROCESS) ) - (forall sl1 signal + (forall sl1 waveform (and (CTL_verifies ps (implies @@ -11,18 +11,16 @@ ) ) (implies - (exists target signal + (exists target waveform (CTL_verifies ps (EF (and (expr_reads sl1) + (expr_writes target) (not - (and - (expr_writes target) - (AX - (AF - (expr_writes target) - ) + (AX + (AF + (expr_writes target) ) ) ) |