[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Re: Is it possible to TLA+ (and PlusCal) to check complex models?

From: Markus Alexander Kuppe <tlaplus-go...@xxxxxxxxxxx>
Date: Sat, 25 Feb 2017 14:55:01 +0100
References: <266afbdf-d8ae-4bbc-baa2-5aecfad375ca@googlegroups.com> <4ba552d4-25c3-44ba-998e-0b280abbd855@googlegroups.com>
User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.7.0

On 24.02.2017 23:19, Hillel Wayne wrote:
> IIRC liveness checking only uses a single core, because it has to track
> behaviors.

Hi,

technically, liveness checking - among other things - searches for
strongly connected components. TLC uses Tarjan's algorithm [1], which is
single threaded.

Cheers
Markus

[1]
https://en.wikipedia.org/wiki/Tarjan's_strongly_connected_components_algorithm

References:
- Is it possible to TLA+ (and PlusCal) to check complex models?
  - From: Shuai Mu
- Re: Is it possible to TLA+ (and PlusCal) to check complex models?
  - From: Hillel Wayne

Prev by Date: Re: Is it possible to TLA+ (and PlusCal) to check complex models?
Next by Date: Re: Is it possible to TLA+ (and PlusCal) to check complex models?
Previous by thread: Re: Is it possible to TLA+ (and PlusCal) to check complex models?
Next by thread: Regarding TLA+ coding
Index(es):
- Date
- Thread