head 1.3; access; symbols pkgsrc-2026Q1:1.3.0.22 pkgsrc-2026Q1-base:1.3 pkgsrc-2025Q4:1.3.0.20 pkgsrc-2025Q4-base:1.3 pkgsrc-2025Q3:1.3.0.18 pkgsrc-2025Q3-base:1.3 pkgsrc-2025Q2:1.3.0.16 pkgsrc-2025Q2-base:1.3 pkgsrc-2025Q1:1.3.0.14 pkgsrc-2025Q1-base:1.3 pkgsrc-2024Q4:1.3.0.12 pkgsrc-2024Q4-base:1.3 pkgsrc-2024Q3:1.3.0.10 pkgsrc-2024Q3-base:1.3 pkgsrc-2024Q2:1.3.0.8 pkgsrc-2024Q2-base:1.3 pkgsrc-2024Q1:1.3.0.6 pkgsrc-2024Q1-base:1.3 pkgsrc-2023Q4:1.3.0.4 pkgsrc-2023Q4-base:1.3 pkgsrc-2023Q3:1.3.0.2 pkgsrc-2023Q3-base:1.3 pkgsrc-2023Q2:1.2.0.46 pkgsrc-2023Q2-base:1.2 pkgsrc-2023Q1:1.2.0.44 pkgsrc-2023Q1-base:1.2 pkgsrc-2022Q4:1.2.0.42 pkgsrc-2022Q4-base:1.2 pkgsrc-2022Q3:1.2.0.40 pkgsrc-2022Q3-base:1.2 pkgsrc-2022Q2:1.2.0.38 pkgsrc-2022Q2-base:1.2 pkgsrc-2022Q1:1.2.0.36 pkgsrc-2022Q1-base:1.2 pkgsrc-2021Q4:1.2.0.34 pkgsrc-2021Q4-base:1.2 pkgsrc-2021Q3:1.2.0.32 pkgsrc-2021Q3-base:1.2 pkgsrc-2021Q2:1.2.0.30 pkgsrc-2021Q2-base:1.2 pkgsrc-2021Q1:1.2.0.28 pkgsrc-2021Q1-base:1.2 pkgsrc-2020Q4:1.2.0.26 pkgsrc-2020Q4-base:1.2 pkgsrc-2020Q3:1.2.0.24 pkgsrc-2020Q3-base:1.2 pkgsrc-2020Q2:1.2.0.22 pkgsrc-2020Q2-base:1.2 pkgsrc-2020Q1:1.2.0.18 pkgsrc-2020Q1-base:1.2 pkgsrc-2019Q4:1.2.0.20 pkgsrc-2019Q4-base:1.2 pkgsrc-2019Q3:1.2.0.16 pkgsrc-2019Q3-base:1.2 pkgsrc-2019Q2:1.2.0.14 pkgsrc-2019Q2-base:1.2 pkgsrc-2019Q1:1.2.0.12 pkgsrc-2019Q1-base:1.2 pkgsrc-2018Q4:1.2.0.10 pkgsrc-2018Q4-base:1.2 pkgsrc-2018Q3:1.2.0.8 pkgsrc-2018Q3-base:1.2 pkgsrc-2018Q2:1.2.0.6 pkgsrc-2018Q2-base:1.2 pkgsrc-2018Q1:1.2.0.4 pkgsrc-2018Q1-base:1.2 pkgsrc-2017Q4:1.2.0.2 pkgsrc-2017Q4-base:1.2 pkgsrc-2017Q3:1.1.1.1.0.58 pkgsrc-2017Q3-base:1.1.1.1 pkgsrc-2017Q2:1.1.1.1.0.54 pkgsrc-2017Q2-base:1.1.1.1 pkgsrc-2017Q1:1.1.1.1.0.52 pkgsrc-2017Q1-base:1.1.1.1 pkgsrc-2016Q4:1.1.1.1.0.50 pkgsrc-2016Q4-base:1.1.1.1 pkgsrc-2016Q3:1.1.1.1.0.48 pkgsrc-2016Q3-base:1.1.1.1 pkgsrc-2016Q2:1.1.1.1.0.46 pkgsrc-2016Q2-base:1.1.1.1 pkgsrc-2016Q1:1.1.1.1.0.44 pkgsrc-2016Q1-base:1.1.1.1 pkgsrc-2015Q4:1.1.1.1.0.42 pkgsrc-2015Q4-base:1.1.1.1 pkgsrc-2015Q3:1.1.1.1.0.40 pkgsrc-2015Q3-base:1.1.1.1 pkgsrc-2015Q2:1.1.1.1.0.38 pkgsrc-2015Q2-base:1.1.1.1 pkgsrc-2015Q1:1.1.1.1.0.36 pkgsrc-2015Q1-base:1.1.1.1 pkgsrc-2014Q4:1.1.1.1.0.34 pkgsrc-2014Q4-base:1.1.1.1 pkgsrc-2014Q3:1.1.1.1.0.32 pkgsrc-2014Q3-base:1.1.1.1 pkgsrc-2014Q2:1.1.1.1.0.30 pkgsrc-2014Q2-base:1.1.1.1 pkgsrc-2014Q1:1.1.1.1.0.28 pkgsrc-2014Q1-base:1.1.1.1 pkgsrc-2013Q4:1.1.1.1.0.26 pkgsrc-2013Q4-base:1.1.1.1 pkgsrc-2013Q3:1.1.1.1.0.24 pkgsrc-2013Q3-base:1.1.1.1 pkgsrc-2013Q2:1.1.1.1.0.22 pkgsrc-2013Q2-base:1.1.1.1 pkgsrc-2013Q1:1.1.1.1.0.20 pkgsrc-2013Q1-base:1.1.1.1 pkgsrc-2012Q4:1.1.1.1.0.18 pkgsrc-2012Q4-base:1.1.1.1 pkgsrc-2012Q3:1.1.1.1.0.16 pkgsrc-2012Q3-base:1.1.1.1 pkgsrc-2012Q2:1.1.1.1.0.14 pkgsrc-2012Q2-base:1.1.1.1 pkgsrc-2012Q1:1.1.1.1.0.12 pkgsrc-2012Q1-base:1.1.1.1 pkgsrc-2011Q4:1.1.1.1.0.10 pkgsrc-2011Q4-base:1.1.1.1 pkgsrc-2011Q3:1.1.1.1.0.8 pkgsrc-2011Q3-base:1.1.1.1 pkgsrc-2011Q2:1.1.1.1.0.6 pkgsrc-2011Q2-base:1.1.1.1 pkgsrc-2011Q1:1.1.1.1.0.4 pkgsrc-2011Q1-base:1.1.1.1 pkgsrc-2010Q4:1.1.1.1.0.2 pkgsrc-2010Q4-base:1.1.1.1 pkgsrc-base:1.1.1.1 TNF:1.1.1; locks; strict; comment @# @; 1.3 date 2023.07.11.11.07.05; author wiz; state Exp; branches; next 1.2; commitid 857z5vs31QJqjnwE; 1.2 date 2017.12.10.13.56.34; author adam; state Exp; branches; next 1.1; commitid O0Nw5lfOBH5bNliA; 1.1 date 2010.10.24.18.54.12; author agc; state Exp; branches 1.1.1.1; next ; 1.1.1.1 date 2010.10.24.18.54.12; author agc; state Exp; branches; next ; desc @@ 1.3 log @spin: update to 6.5.2. No changelog found, couple of years of development. pkgsrc change: Install examples. @ text @@@comment $NetBSD$ bin/spin man/man1/spin.1 share/examples/spin/Book_1991/App.F.datalink.h share/examples/spin/Book_1991/App.F.defines.h share/examples/spin/Book_1991/App.F.flow_cl.h share/examples/spin/Book_1991/App.F.fserver.h share/examples/spin/Book_1991/App.F.pftp.pml share/examples/spin/Book_1991/App.F.present.h share/examples/spin/Book_1991/App.F.session.h share/examples/spin/Book_1991/App.F.user.h share/examples/spin/Book_1991/README.txt share/examples/spin/Book_1991/p101.pml share/examples/spin/Book_1991/p102.pml share/examples/spin/Book_1991/p104.1.pml share/examples/spin/Book_1991/p104.2.pml share/examples/spin/Book_1991/p105.1.pml share/examples/spin/Book_1991/p105.2.pml share/examples/spin/Book_1991/p107.pml share/examples/spin/Book_1991/p108.pml share/examples/spin/Book_1991/p116.pml share/examples/spin/Book_1991/p117.pml share/examples/spin/Book_1991/p123.pml share/examples/spin/Book_1991/p248.pml share/examples/spin/Book_1991/p312.pml share/examples/spin/Book_1991/p319.pml share/examples/spin/Book_1991/p320.pml share/examples/spin/Book_1991/p325.test.h share/examples/spin/Book_1991/p327.upper.h share/examples/spin/Book_1991/p329.pml share/examples/spin/Book_1991/p330.pml share/examples/spin/Book_1991/p337.defines2.h share/examples/spin/Book_1991/p337.fserver.h share/examples/spin/Book_1991/p337.pftp.ses.pml share/examples/spin/Book_1991/p337.session.h share/examples/spin/Book_1991/p337.user.h share/examples/spin/Book_1991/p342.pftp.ses1.h share/examples/spin/Book_1991/p343.claim.h share/examples/spin/Book_1991/p347.pftp.ses5.pml share/examples/spin/Book_1991/p347.pres.sim.h share/examples/spin/Book_1991/p347.session.prog.h share/examples/spin/Book_1991/p94.pml share/examples/spin/Book_1991/p95.1.pml share/examples/spin/Book_1991/p95.2.pml share/examples/spin/Book_1991/p96.1.pml share/examples/spin/Book_1991/p96.2.pml share/examples/spin/Book_1991/p97.1.pml share/examples/spin/Book_1991/p97.2.pml share/examples/spin/Book_1991/p99.pml share/examples/spin/Exercises/ex_1a.pml share/examples/spin/Exercises/ex_1f.pml share/examples/spin/Exercises/ex_2.pml share/examples/spin/Exercises/ex_3a.pml share/examples/spin/Exercises/ex_3b.pml share/examples/spin/Exercises/ex_3c.pml share/examples/spin/Exercises/ex_4.pml share/examples/spin/Exercises/ex_5.pml share/examples/spin/Exercises/ex_6.pml share/examples/spin/LTL/bakery.pml share/examples/spin/LTL/diskhead.pml share/examples/spin/LTL/leader.pml share/examples/spin/LTL/leader_pre.pml share/examples/spin/LTL/ltl_always_eventually.pml share/examples/spin/LTL/ltl_example.pml share/examples/spin/LTL/ltl_gen.pml share/examples/spin/LTL/mobile1.pml share/examples/spin/LTL/mobile2.pml share/examples/spin/LTL/patterns.pml share/examples/spin/LTL/petersonN.pml share/examples/spin/LTL/pftp.pml share/examples/spin/LTL/salesman1.pml share/examples/spin/LTL/salesman2.pml share/examples/spin/LTL/train.pml share/examples/spin/LTL/zune.pml share/examples/spin/README_tests.txt share/examples/spin/abp.pml share/examples/spin/calculator.pml share/examples/spin/cambridge.pml share/examples/spin/dtp.pml share/examples/spin/eratosthenes.pml share/examples/spin/for_example.pml share/examples/spin/for_select_example.pml share/examples/spin/hajek.pml share/examples/spin/hello.pml share/examples/spin/leader0.pml share/examples/spin/leader_trace.pml share/examples/spin/life.pml share/examples/spin/loops.pml share/examples/spin/manna_pnueli.pml share/examples/spin/pathfinder.pml share/examples/spin/peterson.pml share/examples/spin/priorities.pml share/examples/spin/rtos1.pml share/examples/spin/sat.pml share/examples/spin/snoopy.pml share/examples/spin/sort.pml share/examples/spin/test_mtype.pml share/examples/spin/welfare.pml share/examples/spin/werkplaats.pml share/examples/spin/wordcount.pml @ 1.2 log @spin: updated to 6.4.7 Version 6.4.7: - fixed a bug in the parsing of for (...) statements if initialized variable declarations appear in the body of the loop - optimization in interpreting the swarm option, by avoiding unnecessary recompilations, plus other small fixes in the generation of parameter values for -k and -w with swarms - added runtime option -W to suppress recompilation of pan if the executable already exists - fixed bug in printing the value of a random seed at the end of a randomized run - added compilation warning if both -DNP and -DNOCLAIM are used (in that case -DNP is assumed to override -DNOCLAIM) - fixed a bug in the parsing of select (...) statements that could cause unwarranted syntax errors when larger ranges are used - switched to executables for Windows PCs that do not require a cygwin installation (using mingw32 and mingw64 bit compilations) @ text @d1 1 a1 1 @@comment $NetBSD: PLIST,v 1.1.1.1 2010/10/24 18:54:12 agc Exp $ d4 97 @ 1.1 log @Initial revision @ text @d1 1 a1 1 @@comment $NetBSD$ d3 1 a3 1 ${PKGMANDIR}/man1/spin.1 @ 1.1.1.1 log @Initial import of spin version 5.2.5 into the Packages Collection. To verify a design, a formal model is built using PROMELA, Spin's input language. PROMELA is a non-deterministic language, loosely based on Dijkstra's guarded command language notation and borrowing the notation for I/O operations from Hoare's CSP language. Spin can be used in four main modes: 1. as a simulator, allowing for rapid prototyping with a random, guided, or interactive simulations 2. as an exhaustive verifier, capable of rigorously proving the validity of user specified correctness requirements (using partial order reduction theory to optimize the search) 3. as proof approximation system that can validate even very large system models with maximal coverage of the state space. 4. as a driver for swarm verification (a new form of swarm computing), which can make optimal use of large numbers of available compute cores to leverage parallelism and search diversification techniques, which increases the chance of locating defects in very large verification models. With thanks to the plan9 guys for the nudge @ text @@