Faq.Faqs History

Hide minor edits - Show changes to output - Cancel

Changed lines 38-39 from:
'''A:''' The SMT-LIB format is combinational in nature (similarly to a DIMACS file in the pure-boolean case). Thus, you can not save the content of a nuXmv input file (i.e. a transition system plus a set of properties) in SMT-LIB.
However, some of the algorithms of nuXmv allow you to save combinational problems that result from the analysis of transition systems (e.g. the unrolling up to a given depth of a bounded model checking problem).
to:
'''A:''' The SMT-LIB format is combinational in nature (similarly to a DIMACS file in the pure-boolean case). [[<<]] Thus, you can not save the content of a nuXmv input file (i.e. a transition system plus a set of properties) [[<<]] in SMT-LIB.
However, some of the algorithms of nuXmv allow you to save combinational problems that result [[<<]] from the analysis of transition systems (e.g. the unrolling up to a given depth of a bounded model checking problem).
Changed line 11 from:
** Examples of purposes would be running business operations, licensing, leasing, [[<<]] or selling the Software, distributing the Software for use with commercial or non-commercial products, using the Software in the creation or use of commercial or non-commercial products.
to:
** Examples of purposes would be running business operations, licensing, leasing, [[<<]] or selling the Software, distributing the Software for use with commercial or [[<<]] non-commercial products, using the Software in the creation or use of commercial [[<<]] or non-commercial products.
Changed line 11 from:
** Examples of purposes would be running business operations, licensing, leasing, or selling the Software, distributing the Software for use with commercial or non-commercial products, using the Software in the creation or use of commercial or non-commercial products.
to:
** Examples of purposes would be running business operations, licensing, leasing, [[<<]] or selling the Software, distributing the Software for use with commercial or non-commercial products, using the Software in the creation or use of commercial or non-commercial products.
Changed line 6 from:
academic, non-commercial reaserch purposes, subject to the restrictions
to:
academic, [[<<]] non-commercial reaserch purposes, subject to the restrictions
Changed line 12 from:
(Further details are available in the [[Main.License|License]] page.)
to:
Further details are available in the [[Main.License|License]] page.
Changed lines 11-12 from:
** Examples of purposes would be running business operations, licensing, leasing, or selling the Software, distributing the Software for use with commercial or non-commercial products, using the Software in\\the creation or use of commercial or non-commercial products.
to:
** Examples of purposes would be running business operations, licensing, leasing, or selling the Software, distributing the Software for use with commercial or non-commercial products, using the Software in the creation or use of commercial or non-commercial products.
Changed lines 5-6 from:
'''A:''' You may study, copy, compile and execute nuXmv only for\\
academic, non-commercial reaserch purposes, subject to the restrictions\\
to:
'''A:''' You may study, copy, compile and execute nuXmv only for
academic, non-commercial reaserch purposes, subject to the restrictions
Changed lines 8-11 from:
You may not:\\
* Modify nuXmv for any purpose.\\
* Re-distribute nuXmv in any form for any purposes.\\
** Examples of purposes would be running business operations, licensing,\\leasing, or selling the Software, distributing the Software for use\\with commercial or non-commercial products, using the Software in\\the creation or use of commercial or non-commercial products.\\
to:
You may not:
* Modify nuXmv for any purpose.
* Re-distribute nuXmv in any form for any purposes.
** Examples of purposes would be running business operations, licensing, leasing, or selling the Software, distributing the Software for use with commercial or non-commercial products, using the Software in\\the creation or use of commercial or non-commercial products.
Changed lines 11-14 from:
** Examples of purposes would be running business operations, licensing,\\
leasing, or selling the Software, distributing the Software for use\\
with commercial or non-commercial products, using the Software in\\
the creation or use of commercial or non-commercial products.\\
to:
** Examples of purposes would be running business operations, licensing,\\leasing, or selling the Software, distributing the Software for use\\with commercial or non-commercial products, using the Software in\\the creation or use of commercial or non-commercial products.\\
Changed lines 11-14 from:
** Examples of purposes would be running business operations, licensing,
   leasing, or selling the Software, distributing the Software for use
   with commercial or non-commercial products, using the Software in
   the creation or use of commercial or non-commercial products.\\
to:
** Examples of purposes would be running business operations, licensing,\\
leasing, or selling the Software, distributing
the Software for use\\
with commercial or non-commercial products, using the Software
in\\
the creation or use of commercial or non-commercial products.\\
Changed lines 9-11 from:
- Modify nuXmv for any purpose.\\
- Re-distribute nuXmv in any form for any purposes.\\
-- Examplesof purposes would be running business operations, licensing,
to:
* Modify nuXmv for any purpose.\\
* Re-distribute nuXmv in any form for any purposes.\\
** Examples of purposes would be running business operations, licensing,
Changed lines 14-15 from:
   the creation or use of commercial or non-commercial products.
to:
   the creation or use of commercial or non-commercial products.\\
Changed lines 5-7 from:
'''A:''' You may study, copy, compile and execute nuXmv only for
academic, non-commercial reaserch purposes, subject to the restrictions
reported in the %newwin% [[https://es.fbk.eu/tools/nuxmv/downloads/LICENSE.txt|LICENSE.txt]] (Further details are available in the [[Main.License|License]] page.)
to:
'''A:''' You may study, copy, compile and execute nuXmv only for\\
academic, non-commercial reaserch purposes, subject to the restrictions\\
reported in the %newwin% [[https://es.fbk.eu/tools/nuxmv/downloads/LICENSE.txt|LICENSE.txt]]\\
You may not:\\
- Modify nuXmv for any purpose.\\
- Re-distribute nuXmv in any form for any purposes.\\
-- Examplesof purposes would be running business operations, licensing,
  leasing, or selling the Software, distributing the Software for use
  with commercial or non-commercial products, using the Software in
  the creation or use of commercial or non-commercial products.

(Further details are available in the [[Main.License|License]] page.)
Changed lines 5-7 from:
'''A:'''

You may study, copy, compile and execute nuXmv only for
to:
'''A:''' You may study, copy, compile and execute nuXmv only for
Changed lines 5-6 from:
'''A:''' nuXmv can only be used for non-commercial or academic purposes.
Further details are available in
the [[Main.License|License]] page.
to:
'''A:'''

You may study, copy, compile and execute nuXmv only for
academic, non-commercial reaserch purposes, subject to
the restrictions
reported in the %newwin%
[[https://es.fbk.eu/tools/nuxmv/downloads/LICENSE.txt|LICENSE.txt]] (Further details are available in the [[Main.License|License]] page.)
Changed lines 31-33 from:
'''Q:''' Can I save a file in smt format?\\
'''A:''' The SMT-LIB format is combinational in nature (similarly to a DIMACS file in the pure-boolean case). Thus, you can not save a transition system in SMT-LIB.\\
However, you can save combinational problems that result from the analysis of transition systems (e.g.
the unrolling up to a given depth of a bounded model checking probelm).
to:
'''Q:''' Can I save a file in SMT-LIB format?\\
'''A:''' The SMT-LIB format is combinational in nature (similarly to a DIMACS file in the pure-boolean case). Thus, you can not save the content of a nuXmv input file (i.e. a transition system plus a set of properties) in SMT-LIB.
However, some of
the algorithms of nuXmv allow you to save combinational problems that result from the analysis of transition systems (e.g. the unrolling up to a given depth of a bounded model checking problem).
Changed lines 28-34 from:
* Unsubscribe: send an email to [[mailto:sympa@list.fbk.eu?subject=%20uns%20nuxmv-users|sympa@list.fbk.eu]] with subject '''uns nuxmv-users'''.
to:
* Unsubscribe: send an email to [[mailto:sympa@list.fbk.eu?subject=%20uns%20nuxmv-users|sympa@list.fbk.eu]] with subject '''uns nuxmv-users'''.

[[#faq0004]]'''FAQ 0004''' \\
'''Q:''' Can I save a file in smt format?\\
'''A:''' The SMT-LIB format is combinational in nature (similarly to a DIMACS file in the pure-boolean case). Thus, you can not save a transition system in SMT-LIB.\\
However, you can save combinational problems that result from the analysis of transition systems (e.g. the unrolling up to a given depth of a bounded model checking probelm).

Changed lines 5-6 from:
'''A:''' nuXmv as specified in the [[Main.License|License]] page can be used only for non-commercial or academic purposes.
to:
'''A:''' nuXmv can only be used for non-commercial or academic purposes.
Further details are available in the [[Main.License|License]] page
.
Changed line 10 from:
* Using the %newwin%[[https://nuxmv.fbk.eu/bugs|nuXmv Bug Tracker]] (preferred solution)
to:
* Using the %newwin%[[https://nuxmv.fbk.eu/bugs|nuXmv Bug Tracker]] ''(preferred solution)''
Changed line 10 from:
* Using the [[https://nuxmv.fbk.eu/bugs|nuXmv Bug Tracker]] (preferred solution)
to:
* Using the %newwin%[[https://nuxmv.fbk.eu/bugs|nuXmv Bug Tracker]] (preferred solution)
Changed lines 10-11 from:
* Using the [[https://essvn.fbk.eu/bugs|nuXmv Bug Tracker]] (preferred solution)
to:
* Using the [[https://nuxmv.fbk.eu/bugs|nuXmv Bug Tracker]] (preferred solution)
** If needed use the following credentials
Deleted line 13:
Deleted line 14: