Re: [Qemu-devel] [PATCH 10/16] docs: include formal model for TCG exclusive sections

[Paolo Bonzini]

On 26/09/2016 10:24, Alex Bennée wrote:
>   > + * To verify it:
>   > + *     spin -a docs/event.promela
> 
>   wrong docs name
> 
>   > + *     ./a.out -a
> 
>   Which version of spin did you run? I grabbed the latest src release
>   (http://spinroot.com/spin/Src/src645.tar.gz) and had to manually build
>   the output:
> 
>       ~/src/spin/Src6.4.5/spin -a docs/tcg-exclusive.promela
>       gcc pan.c
>       ../a.out

Oops, fixed now (-a is needed by the way).

Paolo

>   > + *
>   > + * Tunable processor macros: N_CPUS, N_EXCLUSIVE, N_CYCLES, USE_MUTEX,
>   > + *                           TEST_EXPENSIVE.
>   > + */
> 
>   How do you pass these? I tried:
> 
>       ~/src/spin/Src6.4.5/spin -a docs/tcg-exclusive.promela -DN_CPUS=4
>       ~/src/spin/Src6.4.5/spin -a docs/tcg-exclusive.promela -DN_CPUS 4
> 
>   without any joy.